The abstract of the Mizar article:

Preliminaries to Structures

by

Library Committee

Received January 6, 1995

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;