:: STRUCT_0 semantic presentation

begin

definition
attrc1 is strict ;
struct 1-sorted  -> ;
aggr1-sorted(# carrier #) ->  1-sorted ;
sel carrier c1 ->  set ;
end;

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

:: deftheorem Def1 defines empty STRUCT_0:def_1_:_
 for S being 1-sorted holds
( S is empty iff the carrier of S is empty );

registration
cluster strict empty for 1-sorted ;
existence
 ex b1 being 1-sorted st
( b1 is strict & b1 is empty )
proof
take T = 1-sorted(# {} #); ::_thesis: ( T is strict & T is empty )
thus  T is strict ; ::_thesis: T is empty
thus  the carrier of T is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

registration
cluster strict non empty for 1-sorted ;
existence
 ex b1 being 1-sorted st
( b1 is strict & not b1 is empty )
proof
take  1-sorted(# {{}} #) ; ::_thesis: ( 1-sorted(# {{}} #) is strict & not 1-sorted(# {{}} #) is empty )
thus  1-sorted(# {{}} #) is strict ; ::_thesis: not 1-sorted(# {{}} #) is empty
thus  not the carrier of 1-sorted(# {{}} #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

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

registration
let S be non empty 1-sorted ;
cluster the carrier of S ->  non empty ;
coherence
 not the carrier of S is empty 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;
end;

definition
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;
end;

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

definition
let T be 1-sorted ;
func {} T ->  Subset of T equals :: STRUCT_0:def 2
 {} ;
coherence
 {} is Subset of T
proof
 {} = {} the carrier of T ;
hence  {} is Subset of T ; ::_thesis: verum
end;
func [#] T ->  Subset of T equals :: STRUCT_0:def 3
 the carrier of T;
coherence
 the carrier of T is Subset of T
proof
 the carrier of T = [#] the carrier of T ;
hence  the carrier of T is Subset of T ; ::_thesis: verum
end;
end;

:: deftheorem  defines {} STRUCT_0:def_2_:_
 for T being 1-sorted holds {} T = {} ;

:: deftheorem  defines [#] STRUCT_0:def_3_:_
 for T being 1-sorted holds [#] T = the carrier of T;

registration
let T be 1-sorted ;
cluster {} T ->  empty ;
coherence
 {} T is empty ;
end;

registration
let T be empty 1-sorted ;
cluster [#] T ->  empty ;
coherence
 [#] T is empty ;
end;

registration
let T be non empty 1-sorted ;
cluster [#] T ->  non empty ;
coherence
 not [#] T is empty ;
end;

registration
let S be non empty 1-sorted ;
cluster non empty for Element of bool the carrier of S;
existence
 not for b1 being Subset of S holds b1 is empty
proof
take  [#] S ; ::_thesis: not [#] S is empty
thus  not [#] S is empty ; ::_thesis: verum
end;
end;

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

definition
let S be 1-sorted ;
mode ManySortedSet of S is ManySortedSet of the carrier of S;
end;

definition
let S be 1-sorted ;
func id S ->  Function of S,S equals :: STRUCT_0:def 4
 id the carrier of S;
coherence
 id the carrier of S is Function of S,S ;
end;

:: deftheorem  defines id STRUCT_0:def_4_:_
 for S being 1-sorted holds id S = id the carrier of S;

definition
let S be 1-sorted ;
mode sequence of S is sequence of the carrier of S;
end;

definition
let S be 1-sorted ;
let X be set ;
mode PartFunc of S,X is PartFunc of the carrier of S,X;
mode PartFunc of X,S is PartFunc of X, the carrier of S;
end;

definition
let S, T be 1-sorted ;
mode PartFunc of S,T is PartFunc of the carrier of S, the carrier of T;
end;

definition
let S be 1-sorted ;
let x be set ;
predx in S means :: STRUCT_0:def 5
x in the carrier of S;
end;

:: deftheorem  defines in STRUCT_0:def_5_:_
 for S being 1-sorted
for x being set holds
( x in S iff x in the carrier of S );

definition
attrc1 is strict ;
struct ZeroStr  ->  1-sorted ;
aggrZeroStr(# carrier, ZeroF #) ->  ZeroStr ;
sel ZeroF c1 ->  Element of the carrier of c1;
end;

registration
cluster non empty strict for ZeroStr ;
existence
 ex b1 being ZeroStr st
( b1 is strict & not b1 is empty )
proof
set A = the non empty set ;
set a = the Element of the non empty set ;
take  ZeroStr(# the non empty set , the Element of the non empty set #) ; ::_thesis: ( ZeroStr(# the non empty set , the Element of the non empty set #) is strict & not ZeroStr(# the non empty set , the Element of the non empty set #) is empty )
thus  ZeroStr(# the non empty set , the Element of the non empty set #) is strict ; ::_thesis: not ZeroStr(# the non empty set , the Element of the non empty set #) is empty
thus  not the carrier of ZeroStr(# the non empty set , the Element of the non empty set #) is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
end;

definition
attrc1 is strict ;
struct OneStr  ->  1-sorted ;
aggrOneStr(# carrier, OneF #) ->  OneStr ;
sel OneF c1 ->  Element of the carrier of c1;
end;

definition
attrc1 is strict ;
struct ZeroOneStr  ->  ZeroStr , OneStr ;
aggrZeroOneStr(# carrier, ZeroF, OneF #) ->  ZeroOneStr ;
end;

definition
let S be ZeroStr ;
func 0. S ->  Element of S equals :: STRUCT_0:def 6
 the ZeroF of S;
coherence
 the ZeroF of S is Element of S ;
end;

:: deftheorem  defines 0. STRUCT_0:def_6_:_
 for S being ZeroStr holds 0. S = the ZeroF of S;

definition
let S be OneStr ;
func 1. S ->  Element of S equals :: STRUCT_0:def 7
 the OneF of S;
coherence
 the OneF of S is Element of S ;
end;

:: deftheorem  defines 1. STRUCT_0:def_7_:_
 for S being OneStr holds 1. S = the OneF of S;

definition
let S be ZeroOneStr ;
attrS is degenerated  means :Def8: :: STRUCT_0:def 8
 0. S = 1. S;
end;

:: deftheorem Def8 defines degenerated STRUCT_0:def_8_:_
 for S being ZeroOneStr holds
( S is degenerated iff 0. S = 1. S );

definition
let IT be 1-sorted ;
attrIT is trivial  means :Def9: :: STRUCT_0:def 9
 the carrier of IT is trivial ;
end;

:: deftheorem Def9 defines trivial STRUCT_0:def_9_:_
 for IT being 1-sorted holds
( IT is trivial iff the carrier of IT is trivial );

registration
cluster empty  ->  trivial for 1-sorted ;
coherence
 for b1 being 1-sorted st b1 is empty holds
b1 is trivial
proof
let S be 1-sorted ; ::_thesis: ( S is empty implies S is trivial )
assume  the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is trivial
hence  the carrier of S is trivial ; :: according to STRUCT_0:def_9 ::_thesis: verum
end;
cluster non trivial  ->  non empty for 1-sorted ;
coherence
 for b1 being 1-sorted st not b1 is trivial holds
not b1 is empty ;
end;

definition
let S be 1-sorted ;
redefine attr S is trivial  means :Def10: :: STRUCT_0:def 10
 for x, y being Element of S holds x = y;
compatibility
 ( S is trivial iff for x, y being Element of S holds x = y )
proof
set I = the carrier of S;
percases ( not the carrier of S is empty or the carrier of S is empty ) ;
supposeA1: not the carrier of S is empty ; ::_thesis: ( S is trivial iff for x, y being Element of S holds x = y )
thus  ( S is trivial implies for x, y being Element of the carrier of S holds x = y ) ::_thesis: ( ( for x, y being Element of S holds x = y ) implies S is trivial )
proof
assume A2: the carrier of S is trivial ; :: according to STRUCT_0:def_9 ::_thesis: for x, y being Element of the carrier of S holds x = y
let x, y be Element of the carrier of S; ::_thesis: x = y
thus  x = y by A2, A1, ZFMISC_1:def_10; ::_thesis: verum
end;
assume A3: for x, y being Element of the carrier of S holds x = y ; ::_thesis: S is trivial
let x, y be set ; :: according to ZFMISC_1:def_10,STRUCT_0:def_9 ::_thesis: ( not x in the carrier of S or not y in the carrier of S or x = y )
thus  ( not x in the carrier of S or not y in the carrier of S or x = y ) by A3; ::_thesis: verum
end;
supposeA4: the carrier of S is empty ; ::_thesis: ( S is trivial iff for x, y being Element of S holds x = y )
 for x, y being Element of the carrier of S holds x = y
proof
let x, y be Element of the carrier of S; ::_thesis: x = y
thus x = {} by A4, SUBSET_1:def_1
.= y by A4, SUBSET_1:def_1 ; ::_thesis: verum
end;
hence  ( S is trivial iff for x, y being Element of S holds x = y ) by A4; ::_thesis: verum
end;
end;
end;
end;

:: deftheorem Def10 defines trivial STRUCT_0:def_10_:_
 for S being 1-sorted holds
( S is trivial iff for x, y being Element of S holds x = y );

registration
cluster non degenerated  ->  non trivial for ZeroOneStr ;
coherence
 for b1 being ZeroOneStr st not b1 is degenerated holds
not b1 is trivial
proof
let L be ZeroOneStr ; ::_thesis: ( not L is degenerated implies not L is trivial )
assume A1: not L is degenerated ; ::_thesis: not L is trivial
assume  L is trivial ; ::_thesis: contradiction
then  0. L = 1. L by Def10;
hence  contradiction by A1, Def8; ::_thesis: verum
end;
end;

registration
cluster strict non empty trivial for 1-sorted ;
existence
 ex b1 being 1-sorted st
( b1 is trivial & not b1 is empty & b1 is strict )
proof
take  1-sorted(# 1 #) ; ::_thesis: ( 1-sorted(# 1 #) is trivial & not 1-sorted(# 1 #) is empty & 1-sorted(# 1 #) is strict )
thus  ( 1-sorted(# 1 #) is trivial & not 1-sorted(# 1 #) is empty & 1-sorted(# 1 #) is strict ) by Def9, CARD_1:49; ::_thesis: verum
end;
cluster strict non trivial for 1-sorted ;
existence
 ex b1 being 1-sorted st
( not b1 is trivial & b1 is strict )
proof
take Y = 1-sorted(# 2 #); ::_thesis: ( not Y is trivial & Y is strict )
reconsider x = 0 , y = 1 as Element of Y by CARD_1:50, TARSKI:def_2;
 x <> y ;
hence  ( not Y is trivial & Y is strict ) by Def10; ::_thesis: verum
end;
end;

registration
let S be non trivial 1-sorted ;
cluster the carrier of S ->  non trivial ;
coherence
 not the carrier of S is trivial by Def9;
end;

registration
let S be trivial 1-sorted ;
cluster the carrier of S ->  trivial ;
coherence
 the carrier of S is trivial by Def9;
end;

begin

definition
let S be 1-sorted ;
attrS is finite  means :Def11: :: STRUCT_0:def 11
 the carrier of S is finite ;
end;

:: deftheorem Def11 defines finite STRUCT_0:def_11_:_
 for S being 1-sorted holds
( S is finite iff the carrier of S is finite );

registration
cluster strict non empty finite for 1-sorted ;
existence
 ex b1 being 1-sorted st
( b1 is strict & b1 is finite & not b1 is empty )
proof
take  1-sorted(# {{}} #) ; ::_thesis: ( 1-sorted(# {{}} #) is strict & 1-sorted(# {{}} #) is finite & not 1-sorted(# {{}} #) is empty )
thus  ( 1-sorted(# {{}} #) is strict & 1-sorted(# {{}} #) is finite & not 1-sorted(# {{}} #) is empty ) by Def11; ::_thesis: verum
end;
end;

registration
let S be finite 1-sorted ;
cluster the carrier of S ->  finite ;
coherence
 the carrier of S is finite by Def11;
end;

registration
cluster empty  ->  empty finite for 1-sorted ;
coherence
 for b1 being empty 1-sorted holds b1 is finite
proof
let S be empty 1-sorted ; ::_thesis: S is finite
thus  the carrier of S is finite ; :: according to STRUCT_0:def_11 ::_thesis: verum
end;
end;

notation
let S be 1-sorted ;
antonym  infinite S for  finite ;
end;

registration
cluster strict infinite for 1-sorted ;
existence
 ex b1 being 1-sorted st
( b1 is strict & b1 is infinite )
proof
take A = 1-sorted(# the infinite set #); ::_thesis: ( A is strict & A is infinite )
thus  A is strict ; ::_thesis: A is infinite
thus  the carrier of A is infinite ; :: according to STRUCT_0:def_11 ::_thesis: verum
end;
end;

registration
let S be infinite 1-sorted ;
cluster the carrier of S ->  infinite ;
coherence
 not the carrier of S is finite by Def11;
end;

registration
cluster infinite  ->  non empty infinite for 1-sorted ;
coherence
 for b1 being infinite 1-sorted holds not b1 is empty ;
end;

registration
cluster trivial  ->  finite for 1-sorted ;
coherence
 for b1 being 1-sorted st b1 is trivial holds
b1 is finite
proof
let S be 1-sorted ; ::_thesis: ( S is trivial implies S is finite )
assume  S is trivial ; ::_thesis: S is finite
then reconsider C = the carrier of S as trivial set ;
 C is finite ;
hence  the carrier of S is finite ; :: according to STRUCT_0:def_11 ::_thesis: verum
end;
end;

registration
cluster infinite  ->  non trivial for 1-sorted ;
coherence
 for b1 being 1-sorted st b1 is infinite holds
not b1 is trivial ;
end;

definition
let S be ZeroStr ;
let x be Element of S;
attrx is zero  means :Def12: :: STRUCT_0:def 12
x = 0. S;
end;

:: deftheorem Def12 defines zero STRUCT_0:def_12_:_
 for S being ZeroStr
for x being Element of S holds
( x is zero iff x = 0. S );

registration
let S be ZeroStr ;
cluster 0. S ->  zero ;
coherence
 0. S is zero by Def12;
end;

registration
cluster strict non degenerated for ZeroOneStr ;
existence
 ex b1 being ZeroOneStr st
( b1 is strict & not b1 is degenerated )
proof
take S = ZeroOneStr(# 2,(In (0,2)),(In (1,2)) #); ::_thesis: ( S is strict & not S is degenerated )
 0 in 2 by CARD_1:50, TARSKI:def_2;
then  ( 1 in 2 & In (0,2) = 0 ) by CARD_1:50, FUNCT_7:def_1, TARSKI:def_2;
then  0. S <> 1. S by FUNCT_7:def_1;
hence  ( S is strict & not S is degenerated ) by Def8; ::_thesis: verum
end;
end;

registration
let S be non degenerated ZeroOneStr ;
cluster 1. S ->  non zero ;
coherence
 not 1. S is zero
proof
 0. S <> 1. S by Def8;
hence  not 1. S is zero by Def12; ::_thesis: verum
end;
end;

definition
let S be 1-sorted ;
mode Cover of S is Cover of the carrier of S;
end;

registration
let S be 1-sorted ;
cluster [#] S ->  non proper ;
coherence
 not [#] S is proper
proof
thus  [#] S = the carrier of S ; :: according to SUBSET_1:def_6 ::_thesis: verum
end;
end;

begin

definition
attrc1 is strict ;
struct 2-sorted  ->  1-sorted ;
aggr2-sorted(# carrier, carrier' #) ->  2-sorted ;
sel carrier' c1 ->  set ;
end;

definition
let S be 2-sorted ;
attrS is void  means :Def13: :: STRUCT_0:def 13
 the carrier' of S is empty ;
end;

:: deftheorem Def13 defines void STRUCT_0:def_13_:_
 for S being 2-sorted holds
( S is void iff the carrier' of S is empty );

registration
cluster empty strict void for 2-sorted ;
existence
 ex b1 being 2-sorted st
( b1 is strict & b1 is empty & b1 is void )
proof
take S = 2-sorted(# {},{} #); ::_thesis: ( S is strict & S is empty & S is void )
thus  S is strict ; ::_thesis: ( S is empty & S is void )
thus  the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is void
thus  the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
end;

registration
let S be void 2-sorted ;
cluster the carrier' of S ->  empty ;
coherence
 the carrier' of S is empty by Def13;
end;

registration
cluster non empty strict non void for 2-sorted ;
existence
 ex b1 being 2-sorted st
( b1 is strict & not b1 is empty & not b1 is void )
proof
take S = 2-sorted(# 1,1 #); ::_thesis: ( S is strict & not S is empty & not S is void )
thus  S is strict ; ::_thesis: ( not S is empty & not S is void )
thus  not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: not S is void
thus  not the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
end;

registration
let S be non void 2-sorted ;
cluster the carrier' of S ->  non empty ;
coherence
 not the carrier' of S is empty by Def13;
end;

definition
let X be 1-sorted ;
let Y be non empty 1-sorted ;
let y be Element of Y;
funcX --> y ->  Function of X,Y equals :: STRUCT_0:def 14
 the carrier of X --> y;
coherence
 the carrier of X --> y is Function of X,Y ;
end;

:: deftheorem  defines --> STRUCT_0:def_14_:_
 for X being 1-sorted
for Y being non empty 1-sorted
for y being Element of Y holds X --> y = the carrier of X --> y;

registration
let S be ZeroStr ;
cluster zero for Element of the carrier of S;
existence
 ex b1 being Element of S st b1 is zero
proof
take  0. S ; ::_thesis: 0. S is zero
thus  0. S = 0. S ; :: according to STRUCT_0:def_12 ::_thesis: verum
end;
end;

registration
cluster strict non trivial for ZeroStr ;
existence
 ex b1 being ZeroStr st
( b1 is strict & not b1 is trivial )
proof
take  ZeroStr(# 2,(In (0,2)) #) ; ::_thesis: ( ZeroStr(# 2,(In (0,2)) #) is strict & not ZeroStr(# 2,(In (0,2)) #) is trivial )
 ( 0 in 2 & 1 in 2 ) by CARD_1:50, TARSKI:def_2;
hence  ( ZeroStr(# 2,(In (0,2)) #) is strict & not ZeroStr(# 2,(In (0,2)) #) is trivial ) by Def10; ::_thesis: verum
end;
end;

registration
let S be non trivial ZeroStr ;
cluster non zero for Element of the carrier of S;
existence
 not for b1 being Element of S holds b1 is zero
proof
consider x, y being Element of S such that
A1: x <> y by Def10;
percases ( x <> 0. S or y <> 0. S ) by A1;
supposeA2: x <> 0. S ; ::_thesis: not for b1 being Element of S holds b1 is zero
take  x ; ::_thesis: not x is zero
thus  x <> 0. S by A2; :: according to STRUCT_0:def_12 ::_thesis: verum
end;
supposeA3: y <> 0. S ; ::_thesis: not for b1 being Element of S holds b1 is zero
take  y ; ::_thesis: not y is zero
thus  y <> 0. S by A3; :: according to STRUCT_0:def_12 ::_thesis: verum
end;
end;
end;
end;

definition
let X be set ;
let S be ZeroStr ;
let R be Relation of X, the carrier of S;
attrR is non-zero  means :: STRUCT_0:def 15
 not 0. S in rng R;
end;

:: deftheorem  defines non-zero STRUCT_0:def_15_:_
 for X being set
for S being ZeroStr
for R being Relation of X, the carrier of S holds
( R is non-zero iff not 0. S in rng R );

definition
let S be 1-sorted ;
func card S ->  Cardinal equals :: STRUCT_0:def 16
 card the carrier of S;
coherence
 card the carrier of S is Cardinal ;
end;

:: deftheorem  defines card STRUCT_0:def_16_:_
 for S being 1-sorted holds card S = card the carrier of S;

definition
let S be 1-sorted ;
mode UnOp of S is UnOp of the carrier of S;
mode BinOp of S is BinOp of the carrier of S;
end;

definition
let S be ZeroStr ;
func NonZero S ->  Subset of S equals :: STRUCT_0:def 17
([#] S) \ {(0. S)};
coherence
 ([#] S) \ {(0. S)} is Subset of S ;
end;

:: deftheorem  defines NonZero STRUCT_0:def_17_:_
 for S being ZeroStr holds NonZero S = ([#] S) \ {(0. S)};

theorem :: STRUCT_0:1
for S being non empty ZeroStr
for u being Element of S holds
( u in NonZero S iff not u is zero )
proof
let S be non empty ZeroStr ; ::_thesis: for u being Element of S holds
( u in NonZero S iff not u is zero )
let u be Element of S; ::_thesis: ( u in NonZero S iff not u is zero )
thus  ( u in NonZero S implies not u is zero ) ::_thesis: ( not u is zero implies u in NonZero S )
proof
assume  u in NonZero S ; ::_thesis: not u is zero
then  u <> 0. S by ZFMISC_1:56;
hence  not u is zero by Def12; ::_thesis: verum
end;
thus  ( not u is zero implies u in NonZero S ) by ZFMISC_1:56; ::_thesis: verum
end;

definition
let V be non empty ZeroStr ;
redefine attr V is trivial  means :Def18: :: STRUCT_0:def 18
 for u being Element of V holds u = 0. V;
compatibility
 ( V is trivial iff for u being Element of V holds u = 0. V )
proof
thus  ( V is trivial implies for a being Element of V holds a = 0. V ) by Def10; ::_thesis: ( ( for u being Element of V holds u = 0. V ) implies V is trivial )
assume A1: for a being Element of V holds a = 0. V ; ::_thesis: V is trivial
let a, b be Element of V; :: according to STRUCT_0:def_10 ::_thesis: a = b
thus a = 0. V by A1
.= b by A1 ; ::_thesis: verum
end;
end;

:: deftheorem Def18 defines trivial STRUCT_0:def_18_:_
 for V being non empty ZeroStr holds
( V is trivial iff for u being Element of V holds u = 0. V );

registration
let V be non trivial ZeroStr ;
cluster NonZero V ->  non empty ;
coherence
 not NonZero V is empty
proof
 ex u being Element of V st u <> 0. V by Def18;
hence  not NonZero V is empty by ZFMISC_1:56; ::_thesis: verum
end;
end;

registration
cluster non empty trivial for ZeroStr ;
existence
 ex b1 being ZeroStr st
( b1 is trivial & not b1 is empty )
proof
take  ZeroStr(# 1,(In (0,1)) #) ; ::_thesis: ( ZeroStr(# 1,(In (0,1)) #) is trivial & not ZeroStr(# 1,(In (0,1)) #) is empty )
thus  ( ZeroStr(# 1,(In (0,1)) #) is trivial & not ZeroStr(# 1,(In (0,1)) #) is empty ) by CARD_1:49; ::_thesis: verum
end;
end;

registration
let S be non empty trivial ZeroStr ;
cluster NonZero S ->  empty ;
coherence
 NonZero S is empty
proof
assume  not NonZero S is empty ; ::_thesis: contradiction
then consider x being Element of S such that
A1: x in NonZero S by SUBSET_1:4;
 not x in {(0. S)} by A1, XBOOLE_0:def_5;
then  x <> 0. S by TARSKI:def_1;
hence  contradiction by Def18; ::_thesis: verum
end;
end;

registration
let S be non empty 1-sorted ;
cluster non empty trivial for Element of bool the carrier of S;
existence
 ex b1 being Subset of S st
( not b1 is empty & b1 is trivial )
proof
 { the Element of S} is Subset of S ;
hence  ex b1 being Subset of S st
( not b1 is empty & b1 is trivial ) ; ::_thesis: verum
end;
end;

theorem :: STRUCT_0:2
for F being non degenerated ZeroOneStr holds 1. F in NonZero F
proof
let F be non degenerated ZeroOneStr ; ::_thesis: 1. F in NonZero F
 not 1. F in {(0. F)} by TARSKI:def_1;
hence  1. F in NonZero F by XBOOLE_0:def_5; ::_thesis: verum
end;

registration
let S be finite 1-sorted ;
cluster card S ->  natural ;
coherence
 card S is natural ;
end;

registration
let S be non empty finite 1-sorted ;
cluster card S ->  non zero for Nat;
coherence
 for b1 being Nat st b1 = card S holds
not b1 is empty ;
end;

registration
let T be non trivial 1-sorted ;
cluster non trivial for Element of bool the carrier of T;
existence
 not for b1 being Subset of T holds b1 is trivial
proof
consider x, y being Element of T such that
A1: x <> y by Def10;
reconsider A = {x,y} as Subset of T ;
take  A ; ::_thesis: not A is trivial
take  x ; :: according to ZFMISC_1:def_10 ::_thesis: ex b1 being set st
( x in A & b1 in A & not x = b1 )
take  y ; ::_thesis: ( x in A & y in A & not x = y )
thus  x in A by TARSKI:def_2; ::_thesis: ( y in A & not x = y )
thus  y in A by TARSKI:def_2; ::_thesis: not x = y
thus  not x = y by A1; ::_thesis: verum
end;
end;

theorem :: STRUCT_0:3
for S being ZeroStr holds not 0. S in NonZero S
proof
let S be ZeroStr ; ::_thesis: not 0. S in NonZero S
assume  0. S in NonZero S ; ::_thesis: contradiction
then  not 0. S in {(0. S)} by XBOOLE_0:def_5;
hence  contradiction by TARSKI:def_1; ::_thesis: verum
end;

theorem :: STRUCT_0:4
for S being non empty ZeroStr holds the carrier of S = {(0. S)} \/ (NonZero S) by XBOOLE_1:45;

definition
let C be set ;
let X be 1-sorted ;
attrX is C -element  means :Def19: :: STRUCT_0:def 19
 the carrier of X is C -element ;
end;

:: deftheorem Def19 defines -element STRUCT_0:def_19_:_
 for C being set
for X being 1-sorted holds
( X is C -element iff the carrier of X is C -element );

registration
let C be Cardinal;
clusterC -element for 1-sorted ;
existence
 ex b1 being 1-sorted st b1 is C -element
proof
take X = 1-sorted(# the C -element set #); ::_thesis: X is C -element
thus  the carrier of X is C -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
end;

registration
let C be Cardinal;
let X be C -element 1-sorted ;
cluster the carrier of X -> C -element ;
coherence
 the carrier of X is C -element by Def19;
end;

registration
cluster empty  ->  0 -element for 1-sorted ;
coherence
 for b1 being 1-sorted st b1 is empty holds
b1 is 0 -element
proof
let S be 1-sorted ; ::_thesis: ( S is empty implies S is 0 -element )
assume  S is empty ; ::_thesis: S is 0 -element
hence  the carrier of S is 0 -element ; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
cluster 0 -element  ->  empty for 1-sorted ;
coherence
 for b1 being 1-sorted st b1 is 0 -element holds
b1 is empty
proof
let S be 1-sorted ; ::_thesis: ( S is 0 -element implies S is empty )
assume  S is 0 -element ; ::_thesis: S is empty
hence  the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: verum
end;
cluster non empty trivial  -> 1 -element for 1-sorted ;
coherence
 for b1 being 1-sorted st not b1 is empty & b1 is trivial holds
b1 is 1 -element
proof
let S be 1-sorted ; ::_thesis: ( not S is empty & S is trivial implies S is 1 -element )
assume A1: not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: ( not S is trivial or S is 1 -element )
assume  S is trivial ; ::_thesis: S is 1 -element
hence  the carrier of S is 1 -element by A1; :: according to STRUCT_0:def_19 ::_thesis: verum
end;
cluster1 -element  ->  non empty trivial for 1-sorted ;
coherence
 for b1 being 1-sorted st b1 is 1 -element holds
( not b1 is empty & b1 is trivial )
proof
let S be 1-sorted ; ::_thesis: ( S is 1 -element implies ( not S is empty & S is trivial ) )
assume A2: S is 1 -element ; ::_thesis: ( not S is empty & S is trivial )
hence  not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is trivial
 the carrier of S is trivial by A2;
hence  S is trivial ; ::_thesis: verum
end;
end;

definition
let S be 2-sorted ;
attrS is feasible  means :Def20: :: STRUCT_0:def 20
( the carrier of S is empty implies the carrier' of S is empty );
end;

:: deftheorem Def20 defines feasible STRUCT_0:def_20_:_
 for S being 2-sorted holds
( S is feasible iff ( the carrier of S is empty implies the carrier' of S is empty ) );

registration
cluster non empty  ->  feasible for 2-sorted ;
coherence
 for b1 being 2-sorted st not b1 is empty holds
b1 is feasible
proof
let S be 2-sorted ; ::_thesis: ( not S is empty implies S is feasible )
assume  not the carrier of S is empty ; :: according to STRUCT_0:def_1 ::_thesis: S is feasible
hence  S is feasible by Def20; ::_thesis: verum
end;
cluster void  ->  feasible for 2-sorted ;
coherence
 for b1 being 2-sorted st b1 is void holds
b1 is feasible
proof
let S be 2-sorted ; ::_thesis: ( S is void implies S is feasible )
assume  the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: S is feasible
hence  S is feasible by Def20; ::_thesis: verum
end;
cluster empty feasible  ->  void for 2-sorted ;
coherence
 for b1 being 2-sorted st b1 is empty & b1 is feasible holds
b1 is void
proof
let S be 2-sorted ; ::_thesis: ( S is empty & S is feasible implies S is void )
assume  ( the carrier of S is empty & S is feasible ) ; :: according to STRUCT_0:def_1 ::_thesis: S is void
hence  the carrier' of S is empty by Def20; :: according to STRUCT_0:def_13 ::_thesis: verum
end;
cluster non void feasible  ->  non empty for 2-sorted ;
coherence
 for b1 being 2-sorted st not b1 is void & b1 is feasible holds
not b1 is empty ;
end;

definition
let S be 2-sorted ;
attrS is trivial'  means :Def21: :: STRUCT_0:def 21
 the carrier' of S is trivial ;
end;

:: deftheorem Def21 defines trivial' STRUCT_0:def_21_:_
 for S being 2-sorted holds
( S is trivial' iff the carrier' of S is trivial );

registration
cluster non empty trivial strict non void trivial' for 2-sorted ;
existence
 ex b1 being 2-sorted st
( b1 is strict & not b1 is empty & not b1 is void & b1 is trivial & b1 is trivial' )
proof
take S = 2-sorted(# 1,1 #); ::_thesis: ( S is strict & not S is empty & not S is void & S is trivial & S is trivial' )
thus  S is strict ; ::_thesis: ( not S is empty & not S is void & S is trivial & S is trivial' )
thus  not S is empty ; ::_thesis: ( not S is void & S is trivial & S is trivial' )
thus  not S is void ; ::_thesis: ( S is trivial & S is trivial' )
thus  S is trivial by CARD_1:49; ::_thesis: S is trivial'
thus  the carrier' of S is trivial by CARD_1:49; :: according to STRUCT_0:def_21 ::_thesis: verum
end;
end;

registration
let S be trivial' 2-sorted ;
cluster the carrier' of S ->  trivial ;
coherence
 the carrier' of S is trivial by Def21;
end;

registration
cluster non trivial' for 2-sorted ;
existence
 not for b1 being 2-sorted holds b1 is trivial'
proof
take S = 2-sorted(# 1,{0,1} #); ::_thesis: not S is trivial'
 ( 0 in {0,1} & 1 in {0,1} ) by TARSKI:def_2;
hence  not S is trivial' by ZFMISC_1:def_10; ::_thesis: verum
end;
end;

registration
let S be non trivial' 2-sorted ;
cluster the carrier' of S ->  non trivial ;
coherence
 not the carrier' of S is trivial by Def21;
end;

registration
cluster void  ->  trivial' for 2-sorted ;
coherence
 for b1 being 2-sorted st b1 is void holds
b1 is trivial'
proof
let S be 2-sorted ; ::_thesis: ( S is void implies S is trivial' )
assume  the carrier' of S is empty ; :: according to STRUCT_0:def_13 ::_thesis: S is trivial'
hence  the carrier' of S is trivial ; :: according to STRUCT_0:def_21 ::_thesis: verum
end;
cluster non trivial  ->  non empty for 1-sorted ;
coherence
 for b1 being 1-sorted st not b1 is trivial holds
not b1 is empty ;
end;