The Mizar article STRUCT

The Mizar article:
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;
 theorems SUBSET_1, SETFAM_1, XBOOLE_1;

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
:Def1:  the carrier of S is empty;
end;

definition
 cluster non empty 1-sorted;
 existence
  proof consider A being non empty set;
   take 1-sorted(#A#);
   thus the carrier of 1-sorted(#A#) is non empty;
  end;
end;

definition
 cluster non empty ZeroStr;
 existence
  proof consider A being non empty set, a being Element of A;
   take ZeroStr(#A,a#);
   thus the carrier of ZeroStr(#A,a#) is non empty;
  end;
end;

definition let S be non empty 1-sorted;
 cluster the carrier of S -> non empty;
 coherence by Def1;
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;
 existence
  proof
   {} c= the carrier of S by XBOOLE_1:2;
   hence thesis;
  end;

 cluster empty Subset-Family of S;
 existence
  proof
     {} c= bool the carrier of S by XBOOLE_1:2;
   then {} is Subset-Family of S by SETFAM_1:def 7;
   hence thesis;
  end;

 cluster non empty Subset-Family of S;
 existence
  proof consider A being non empty Subset of bool the carrier of S;
     A is Subset-Family of S by SETFAM_1:def 7;
   hence thesis;
  end;
end;

definition let S be non empty 1-sorted;
 cluster non empty Subset of S;
 existence
  proof consider A being non empty Subset of S;
   take A;
   thus thesis;
  end;
end;

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

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

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

definition let S be non empty 1-sorted,
               X be non empty Subset of S;
 redefine mode Element of X -> Element of S;
 coherence
  proof
   let x be Element of X;
   thus x is Element of S;
  end;
end;

definition let S be 1-sorted,
               X, Y be Subset-Family of S;
 redefine func X \/ Y -> Subset-Family of S;
 coherence
 proof
   thus X \/ Y is Subset-Family of S by SETFAM_1:def 7;
 end;
 redefine func X /\ Y -> Subset-Family of S;
 coherence
 proof
   thus X /\ Y is Subset-Family of S by SETFAM_1:def 7;
 end;
 redefine func X \ Y -> Subset-Family of S;
 coherence
 proof
   thus X \ Y is Subset-Family of S by SETFAM_1:def 7;
 end;
end;
The Mizar article:

Preliminaries to Structures
