:: 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;