Journal of Formalized Mathematics
University of Bialystok
Copyright (c) 1995 Association of Mizar Users

### Preliminaries to Structures

by
Library Committee

MML identifier: STRUCT_0
[ Mizar article, MML identifier index ]

```environ

vocabulary SETFAM_1, BOOLE;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1;
constructors SETFAM_1, XBOOLE_0;
clusters SUBSET_1, XBOOLE_0, ZFMISC_1;
requirements SUBSET;

begin

definition
struct 1-sorted(# carrier -> set #);
end;

definition
struct (1-sorted) ZeroStr(# carrier -> set,
Zero -> Element of the carrier #);
end;

definition let S be 1-sorted;
attr S is empty means
:: STRUCT_0:def 1
the carrier of S is empty;
end;

definition
cluster non empty 1-sorted;
end;

definition
cluster non empty ZeroStr;
end;

definition let S be non empty 1-sorted;
cluster the carrier of S -> non empty;
end;

definition let S be 1-sorted;
mode Element of S is Element of the carrier of S;
mode Subset of S is Subset of the carrier of S;
mode Subset-Family of S is Subset-Family of the carrier of S;
canceled 3;
end;

definition let S be 1-sorted;
cluster empty Subset of S;

cluster empty Subset-Family of S;

cluster non empty Subset-Family of S;
end;

definition let S be non empty 1-sorted;
cluster non empty Subset of S;
end;

definition let S be 1-sorted, A, B be Subset of S;
canceled;
redefine func A \/ B -> Subset of S;
redefine func A /\ B -> Subset of S;
redefine func A \ B -> Subset of S;
redefine func A \+\ B -> Subset of S;
end;

definition let S be non empty 1-sorted,
a be Element of S;
redefine func {a} -> Subset of S;
end;

definition let S be non empty 1-sorted,
a1, a2 be Element of S;
redefine func {a1,a2} -> Subset of S;
end;

definition let S be non empty 1-sorted,
X be non empty Subset of S;
redefine mode Element of X -> Element of S;
end;

definition let S be 1-sorted,
X, Y be Subset-Family of S;
redefine func X \/ Y -> Subset-Family of S;
redefine func X /\ Y -> Subset-Family of S;
redefine func X \ Y -> Subset-Family of S;
end;
```