attr c₁ is strict;
struct 1-sorted -> ;
aggr 1-sorted(# carrier #) -> 1-sorted ;
sel carrier c₁ -> set ;

attr c₁ is strict;
struct ZeroStr -> 1-sorted ;
aggr ZeroStr(# carrier, Zero #) -> ZeroStr ;
sel Zero c₁ -> Element of the carrier of c₁;

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

cluster non empty 1-sorted ;
existence
not for b₁ being 1-sorted holds b₁ is empty

cluster non empty ZeroStr ;
existence
not for b₁ being ZeroStr holds b₁ is empty

let S be non empty 1-sorted ;
cluster the carrier of S -> non empty ;
coherence
not the carrier of S is empty by Def1;

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;

let S be non empty 1-sorted ;
cluster non empty Element of bool the carrier of S;
existence
not for b₁ being Subset of S holds b₁ is empty

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

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

let S be non empty 1-sorted ;
let X be non empty Subset of S;
:: original: Element
redefine mode Element of X -> Element of S;
coherence
for b₁ being Element of X holds b₁ is Element of S

let S be 1-sorted ;
let X be set ;
mode Function of S,X is Function of the carrier of S,X;
mode Function of X,S is Function of X,the carrier of S;

let S, T be 1-sorted ;
mode Function of S,T is Function of the carrier of S,the carrier of T;

let S be 1-sorted ;
mode FinSequence of S is FinSequence of the carrier of S;