:: LFUZZY_0 semantic presentation begin definition let R be RelStr ; attrR is real means :Def1: :: LFUZZY_0:def 1 ( the carrier of R c= REAL & ( for x, y being real number st x in the carrier of R & y in the carrier of R holds ( [x,y] in the InternalRel of R iff x <= y ) ) ); end; :: deftheorem Def1 defines real LFUZZY_0:def_1_:_ for R being RelStr holds ( R is real iff ( the carrier of R c= REAL & ( for x, y being real number st x in the carrier of R & y in the carrier of R holds ( [x,y] in the InternalRel of R iff x <= y ) ) ) ); definition let R be RelStr ; attrR is interval means :Def2: :: LFUZZY_0:def 2 ( R is real & ex a, b being real number st ( a <= b & the carrier of R = [.a,b.] ) ); end; :: deftheorem Def2 defines interval LFUZZY_0:def_2_:_ for R being RelStr holds ( R is interval iff ( R is real & ex a, b being real number st ( a <= b & the carrier of R = [.a,b.] ) ) ); registration cluster interval -> non empty real for RelStr ; coherence for b1 being RelStr st b1 is interval holds ( b1 is real & not b1 is empty ) proof let R be RelStr ; ::_thesis: ( R is interval implies ( R is real & not R is empty ) ) assume A1: R is real ; :: according to LFUZZY_0:def_2 ::_thesis: ( for a, b being real number holds ( not a <= b or not the carrier of R = [.a,b.] ) or ( R is real & not R is empty ) ) given a, b being real number such that A2: ( a <= b & the carrier of R = [.a,b.] ) ; ::_thesis: ( R is real & not R is empty ) thus R is real by A1; ::_thesis: not R is empty thus not the carrier of R is empty by A2, XXREAL_1:1; :: according to STRUCT_0:def_1 ::_thesis: verum end; end; registration cluster empty -> real for RelStr ; coherence for b1 being RelStr st b1 is empty holds b1 is real proof let R be RelStr ; ::_thesis: ( R is empty implies R is real ) assume A1: the carrier of R is empty ; :: according to STRUCT_0:def_1 ::_thesis: R is real hence the carrier of R c= REAL by XBOOLE_1:2; :: according to LFUZZY_0:def_1 ::_thesis: for x, y being real number st x in the carrier of R & y in the carrier of R holds ( [x,y] in the InternalRel of R iff x <= y ) thus for x, y being real number st x in the carrier of R & y in the carrier of R holds ( [x,y] in the InternalRel of R iff x <= y ) by A1; ::_thesis: verum end; end; theorem Th1: :: LFUZZY_0:1 for X being Subset of REAL ex R being strict RelStr st ( the carrier of R = X & R is real ) proof let X be Subset of REAL; ::_thesis: ex R being strict RelStr st ( the carrier of R = X & R is real ) percases ( X is empty or not X is empty ) ; supposeA1: X is empty ; ::_thesis: ex R being strict RelStr st ( the carrier of R = X & R is real ) set E = the empty strict RelStr ; take the empty strict RelStr ; ::_thesis: ( the carrier of the empty strict RelStr = X & the empty strict RelStr is real ) thus ( the carrier of the empty strict RelStr = X & the empty strict RelStr is real ) by A1; ::_thesis: verum end; suppose not X is empty ; ::_thesis: ex R being strict RelStr st ( the carrier of R = X & R is real ) then reconsider Y = X as non empty set ; defpred S1[ set , set ] means ex x, y being real number st ( \$1 = x & \$2 = y & x <= y ); consider L being non empty strict RelStr such that A2: the carrier of L = Y and A3: for a, b being Element of L holds ( a <= b iff S1[a,b] ) from YELLOW_0:sch_1(); take L ; ::_thesis: ( the carrier of L = X & L is real ) thus the carrier of L = X by A2; ::_thesis: L is real thus the carrier of L c= REAL by A2; :: according to LFUZZY_0:def_1 ::_thesis: for x, y being real number st x in the carrier of L & y in the carrier of L holds ( [x,y] in the InternalRel of L iff x <= y ) let x, y be real number ; ::_thesis: ( x in the carrier of L & y in the carrier of L implies ( [x,y] in the InternalRel of L iff x <= y ) ) assume ( x in the carrier of L & y in the carrier of L ) ; ::_thesis: ( [x,y] in the InternalRel of L iff x <= y ) then reconsider a = x, b = y as Element of L ; ( a <= b iff [x,y] in the InternalRel of L ) by ORDERS_2:def_5; then ( [x,y] in the InternalRel of L iff ex x, y being real number st ( a = x & b = y & x <= y ) ) by A3; hence ( [x,y] in the InternalRel of L iff x <= y ) ; ::_thesis: verum end; end; end; registration cluster strict interval for RelStr ; existence ex b1 being RelStr st ( b1 is interval & b1 is strict ) proof set X = [.0,1.]; consider R being strict RelStr such that A1: ( the carrier of R = [.0,1.] & R is real ) by Th1; take R ; ::_thesis: ( R is interval & R is strict ) thus ( R is interval & R is strict ) by A1, Def2; ::_thesis: verum end; end; theorem Th2: :: LFUZZY_0:2 for R1, R2 being real RelStr st the carrier of R1 = the carrier of R2 holds RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) proof let R1, R2 be real RelStr ; ::_thesis: ( the carrier of R1 = the carrier of R2 implies RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) ) assume A1: the carrier of R1 = the carrier of R2 ; ::_thesis: RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) set X = the carrier of R1; the InternalRel of R1 = the InternalRel of R2 proof let a, b be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [a,b] in the InternalRel of R1 or [a,b] in the InternalRel of R2 ) & ( not [a,b] in the InternalRel of R2 or [a,b] in the InternalRel of R1 ) ) A2: the carrier of R1 c= REAL by Def1; hereby ::_thesis: ( not [a,b] in the InternalRel of R2 or [a,b] in the InternalRel of R1 ) assume A3: [a,b] in the InternalRel of R1 ; ::_thesis: [a,b] in the InternalRel of R2 then A4: ( a in the carrier of R1 & b in the carrier of R1 ) by ZFMISC_1:87; then reconsider a9 = a, b9 = b as Element of REAL by A2; a9 <= b9 by A3, A4, Def1; hence [a,b] in the InternalRel of R2 by A1, A4, Def1; ::_thesis: verum end; assume A5: [a,b] in the InternalRel of R2 ; ::_thesis: [a,b] in the InternalRel of R1 then A6: ( a in the carrier of R1 & b in the carrier of R1 ) by A1, ZFMISC_1:87; then reconsider a9 = a, b9 = b as Element of REAL by A2; a9 <= b9 by A1, A5, A6, Def1; hence [a,b] in the InternalRel of R1 by A6, Def1; ::_thesis: verum end; hence RelStr(# the carrier of R1, the InternalRel of R1 #) = RelStr(# the carrier of R2, the InternalRel of R2 #) by A1; ::_thesis: verum end; registration let R be non empty real RelStr ; cluster -> real for Element of the carrier of R; coherence for b1 being Element of R holds b1 is real proof let x be Element of R; ::_thesis: x is real the carrier of R c= REAL by Def1; hence x is real ; ::_thesis: verum end; end; definition let X be Subset of REAL; func RealPoset X -> strict real RelStr means :Def3: :: LFUZZY_0:def 3 the carrier of it = X; existence ex b1 being strict real RelStr st the carrier of b1 = X proof ex R being strict RelStr st ( the carrier of R = X & R is real ) by Th1; hence ex b1 being strict real RelStr st the carrier of b1 = X ; ::_thesis: verum end; uniqueness for b1, b2 being strict real RelStr st the carrier of b1 = X & the carrier of b2 = X holds b1 = b2 by Th2; end; :: deftheorem Def3 defines RealPoset LFUZZY_0:def_3_:_ for X being Subset of REAL for b2 being strict real RelStr holds ( b2 = RealPoset X iff the carrier of b2 = X ); registration let X be non empty Subset of REAL; cluster RealPoset X -> non empty strict real ; coherence not RealPoset X is empty by Def3; end; notation let R be RelStr ; let x, y be Element of R; synonym x <<= y for x <= y; synonym y >>= x for x <= y; antonym x ~<= y for x <= y; antonym y ~>= x for x <= y; end; theorem Th3: :: LFUZZY_0:3 for R being non empty real RelStr for x, y being Element of R holds ( x <= y iff x <<= y ) proof let R be non empty real RelStr ; ::_thesis: for x, y being Element of R holds ( x <= y iff x <<= y ) let x, y be Element of R; ::_thesis: ( x <= y iff x <<= y ) ( [x,y] in the InternalRel of R iff x <= y ) by Def1; hence ( x <= y iff x <<= y ) by ORDERS_2:def_5; ::_thesis: verum end; registration cluster real -> reflexive transitive antisymmetric for RelStr ; coherence for b1 being RelStr st b1 is real holds ( b1 is reflexive & b1 is antisymmetric & b1 is transitive ) proof let R be RelStr ; ::_thesis: ( R is real implies ( R is reflexive & R is antisymmetric & R is transitive ) ) assume A1: R is real ; ::_thesis: ( R is reflexive & R is antisymmetric & R is transitive ) percases ( R is empty or not R is empty ) ; suppose R is empty ; ::_thesis: ( R is reflexive & R is antisymmetric & R is transitive ) hence ( R is reflexive & R is antisymmetric & R is transitive ) ; ::_thesis: verum end; suppose not R is empty ; ::_thesis: ( R is reflexive & R is antisymmetric & R is transitive ) then reconsider R9 = R as non empty real RelStr by A1; A2: R9 is antisymmetric proof let x, y be Element of R9; :: according to YELLOW_0:def_3 ::_thesis: ( not x <<= y or not y <<= x or x = y ) assume ( x <<= y & x >>= y ) ; ::_thesis: x = y then ( x <= y & x >= y ) by Th3; hence x = y by XXREAL_0:1; ::_thesis: verum end; A3: R9 is transitive proof let x, y, z be Element of R9; :: according to YELLOW_0:def_2 ::_thesis: ( not x <<= y or not y <<= z or x <<= z ) assume ( x <<= y & y <<= z ) ; ::_thesis: x <<= z then ( x <= y & y <= z ) by Th3; then x <= z by XXREAL_0:2; hence x <<= z by Th3; ::_thesis: verum end; R9 is reflexive proof let x be Element of R9; :: according to YELLOW_0:def_1 ::_thesis: x <<= x thus x <<= x by Th3; ::_thesis: verum end; hence ( R is reflexive & R is antisymmetric & R is transitive ) by A2, A3; ::_thesis: verum end; end; end; end; registration cluster non empty real -> non empty connected real for RelStr ; coherence for b1 being non empty real RelStr holds b1 is connected proof let R be non empty real RelStr ; ::_thesis: R is connected let x, y be Element of R; :: according to WAYBEL_0:def_29 ::_thesis: ( x <<= y or y <<= x ) ( x <= y or x >= y ) ; hence ( x <<= y or y <<= x ) by Th3; ::_thesis: verum end; end; definition let R be non empty real RelStr ; let x, y be Element of R; :: original: max redefine func max (x,y) -> Element of R; coherence max (x,y) is Element of R by XXREAL_0:16; end; definition let R be non empty real RelStr ; let x, y be Element of R; :: original: min redefine func min (x,y) -> Element of R; coherence min (x,y) is Element of R by XXREAL_0:15; end; registration cluster non empty real -> non empty with_suprema with_infima real for RelStr ; coherence for b1 being non empty real RelStr holds ( b1 is with_suprema & b1 is with_infima ) ; end; registration let R be non empty real RelStr ; let a, b be Element of R; identifya "\/" b with max (a,b); compatibility a "\/" b = max (a,b) proof A1: for d being Element of R st d >>= a & d >>= b holds max (a,b) <<= d proof let d be Element of R; ::_thesis: ( d >>= a & d >>= b implies max (a,b) <<= d ) assume ( d >>= a & d >>= b ) ; ::_thesis: max (a,b) <<= d then ( d >= a & d >= b ) by Th3; then max (a,b) <= d by XXREAL_0:28; hence max (a,b) <<= d by Th3; ::_thesis: verum end; max (a,b) >= b by XXREAL_0:25; then A2: max (a,b) >>= b by Th3; max (a,b) >= a by XXREAL_0:25; then max (a,b) >>= a by Th3; hence a "\/" b = max (a,b) by A2, A1, YELLOW_0:22; ::_thesis: verum end; identifya "/\" b with min (a,b); compatibility a "/\" b = min (a,b) proof A3: for d being Element of R st d <<= a & d <<= b holds min (a,b) >>= d proof let d be Element of R; ::_thesis: ( d <<= a & d <<= b implies min (a,b) >>= d ) assume ( d <<= a & d <<= b ) ; ::_thesis: min (a,b) >>= d then ( d <= a & d <= b ) by Th3; then d <= min (a,b) by XXREAL_0:20; hence min (a,b) >>= d by Th3; ::_thesis: verum end; min (a,b) <= b by XXREAL_0:17; then A4: min (a,b) <<= b by Th3; min (a,b) <= a by XXREAL_0:17; then min (a,b) <<= a by Th3; hence a "/\" b = min (a,b) by A4, A3, YELLOW_0:23; ::_thesis: verum end; end; theorem :: LFUZZY_0:4 for R being non empty real RelStr for a, b being Element of R holds a "\/" b = max (a,b) ; theorem :: LFUZZY_0:5 for R being non empty real RelStr for a, b being Element of R holds a "/\" b = min (a,b) ; theorem Th6: :: LFUZZY_0:6 for R being non empty real RelStr holds ( ex x being real number st ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x <= y ) ) iff R is lower-bounded ) proof let R be non empty real RelStr ; ::_thesis: ( ex x being real number st ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x <= y ) ) iff R is lower-bounded ) hereby ::_thesis: ( R is lower-bounded implies ex x being real number st ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x <= y ) ) ) given x being real number such that A1: x in the carrier of R and A2: for y being real number st y in the carrier of R holds x <= y ; ::_thesis: R is lower-bounded reconsider a = x as Element of R by A1; now__::_thesis:_for_b_being_Element_of_R_st_b_in_the_carrier_of_R_holds_ a_<<=_b let b be Element of R; ::_thesis: ( b in the carrier of R implies a <<= b ) assume b in the carrier of R ; ::_thesis: a <<= b b >= a by A2; hence a <<= b by Th3; ::_thesis: verum end; then a is_<=_than the carrier of R by LATTICE3:def_8; hence R is lower-bounded by YELLOW_0:def_4; ::_thesis: verum end; given x being Element of R such that A3: x is_<=_than the carrier of R ; :: according to YELLOW_0:def_4 ::_thesis: ex x being real number st ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x <= y ) ) take x ; ::_thesis: ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x <= y ) ) thus x in the carrier of R ; ::_thesis: for y being real number st y in the carrier of R holds x <= y let y be real number ; ::_thesis: ( y in the carrier of R implies x <= y ) assume y in the carrier of R ; ::_thesis: x <= y then reconsider b = y as Element of R ; x <<= b by A3, LATTICE3:def_8; hence x <= y by Th3; ::_thesis: verum end; theorem Th7: :: LFUZZY_0:7 for R being non empty real RelStr holds ( ex x being real number st ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x >= y ) ) iff R is upper-bounded ) proof let R be non empty real RelStr ; ::_thesis: ( ex x being real number st ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x >= y ) ) iff R is upper-bounded ) hereby ::_thesis: ( R is upper-bounded implies ex x being real number st ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x >= y ) ) ) given x being real number such that A1: x in the carrier of R and A2: for y being real number st y in the carrier of R holds x >= y ; ::_thesis: R is upper-bounded reconsider a = x as Element of R by A1; now__::_thesis:_for_b_being_Element_of_R_st_b_in_the_carrier_of_R_holds_ a_>>=_b let b be Element of R; ::_thesis: ( b in the carrier of R implies a >>= b ) assume b in the carrier of R ; ::_thesis: a >>= b a >= b by A2; hence a >>= b by Th3; ::_thesis: verum end; then a is_>=_than the carrier of R by LATTICE3:def_9; hence R is upper-bounded by YELLOW_0:def_5; ::_thesis: verum end; given x being Element of R such that A3: x is_>=_than the carrier of R ; :: according to YELLOW_0:def_5 ::_thesis: ex x being real number st ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x >= y ) ) take x ; ::_thesis: ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x >= y ) ) thus x in the carrier of R ; ::_thesis: for y being real number st y in the carrier of R holds x >= y let y be real number ; ::_thesis: ( y in the carrier of R implies x >= y ) assume y in the carrier of R ; ::_thesis: x >= y then reconsider b = y as Element of R ; x >>= b by A3, LATTICE3:def_9; hence x >= y by Th3; ::_thesis: verum end; registration cluster non empty interval -> non empty bounded for RelStr ; coherence for b1 being non empty RelStr st b1 is interval holds b1 is bounded proof let R be non empty RelStr ; ::_thesis: ( R is interval implies R is bounded ) assume A1: R is real ; :: according to LFUZZY_0:def_2 ::_thesis: ( for a, b being real number holds ( not a <= b or not the carrier of R = [.a,b.] ) or R is bounded ) given x, y being real number such that A2: x <= y and A3: the carrier of R = [.x,y.] ; ::_thesis: R is bounded ex x being real number st ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x <= y ) ) proof take x ; ::_thesis: ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x <= y ) ) thus x in the carrier of R by A2, A3, XXREAL_1:1; ::_thesis: for y being real number st y in the carrier of R holds x <= y let z be real number ; ::_thesis: ( z in the carrier of R implies x <= z ) assume z in the carrier of R ; ::_thesis: x <= z hence x <= z by A3, XXREAL_1:1; ::_thesis: verum end; then A4: R is lower-bounded by A1, Th6; ex x being real number st ( x in the carrier of R & ( for y being real number st y in the carrier of R holds x >= y ) ) proof take y ; ::_thesis: ( y in the carrier of R & ( for y being real number st y in the carrier of R holds y >= y ) ) thus y in the carrier of R by A2, A3, XXREAL_1:1; ::_thesis: for y being real number st y in the carrier of R holds y >= y let z be real number ; ::_thesis: ( z in the carrier of R implies y >= z ) assume z in the carrier of R ; ::_thesis: y >= z hence y >= z by A3, XXREAL_1:1; ::_thesis: verum end; then R is upper-bounded by A1, Th7; hence R is bounded by A4; ::_thesis: verum end; end; theorem Th8: :: LFUZZY_0:8 for R being non empty interval RelStr for X being set holds ex_sup_of X,R proof let R be non empty interval RelStr ; ::_thesis: for X being set holds ex_sup_of X,R let X be set ; ::_thesis: ex_sup_of X,R consider a, b being real number such that A1: a <= b and A2: the carrier of R = [.a,b.] by Def2; reconsider a = a, b = b as Real by XREAL_0:def_1; reconsider Y = X /\ [.a,b.] as Subset of REAL ; ( not [.a,b.] is empty & [.a,b.] is closed_interval ) by A1, MEASURE5:14; then A3: [.a,b.] is bounded_above by INTEGRA1:3; then A4: Y is bounded_above by XBOOLE_1:17, XXREAL_2:43; A5: X /\ [.a,b.] c= [.a,b.] by XBOOLE_1:17; ex a being Element of R st ( Y is_<=_than a & ( for b being Element of R st Y is_<=_than b holds a <<= b ) ) proof percases ( Y is empty or not Y is empty ) ; supposeA6: Y is empty ; ::_thesis: ex a being Element of R st ( Y is_<=_than a & ( for b being Element of R st Y is_<=_than b holds a <<= b ) ) reconsider x = a as Element of R by A1, A2, XXREAL_1:1; take x ; ::_thesis: ( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds x <<= b ) ) thus Y is_<=_than x by A6, YELLOW_0:6; ::_thesis: for b being Element of R st Y is_<=_than b holds x <<= b let y be Element of R; ::_thesis: ( Y is_<=_than y implies x <<= y ) x <= y by A2, XXREAL_1:1; hence ( Y is_<=_than y implies x <<= y ) by Th3; ::_thesis: verum end; supposeA7: not Y is empty ; ::_thesis: ex a being Element of R st ( Y is_<=_than a & ( for b being Element of R st Y is_<=_than b holds a <<= b ) ) set c = the Element of Y; A8: the Element of Y in Y by A7; then reconsider c = the Element of Y as Real ; A9: a <= c by A5, A8, XXREAL_1:1; c <= upper_bound Y by A4, A7, SEQ_4:def_1; then A10: a <= upper_bound Y by A9, XXREAL_0:2; upper_bound [.a,b.] = b by A1, JORDAN5A:19; then upper_bound Y <= b by A3, A7, SEQ_4:48, XBOOLE_1:17; then reconsider x = upper_bound Y as Element of R by A2, A10, XXREAL_1:1; A11: for y being Element of R st Y is_<=_than y holds x <<= y proof let y be Element of R; ::_thesis: ( Y is_<=_than y implies x <<= y ) assume A12: Y is_<=_than y ; ::_thesis: x <<= y for z being real number st z in Y holds z <= y proof let z be real number ; ::_thesis: ( z in Y implies z <= y ) assume A13: z in Y ; ::_thesis: z <= y then reconsider z = z as Element of R by A2, XBOOLE_0:def_4; z <<= y by A12, A13, LATTICE3:def_9; hence z <= y by Th3; ::_thesis: verum end; then upper_bound Y <= y by A7, SEQ_4:144; hence x <<= y by Th3; ::_thesis: verum end; take x ; ::_thesis: ( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds x <<= b ) ) for b being Element of R st b in Y holds b <<= x proof let b be Element of R; ::_thesis: ( b in Y implies b <<= x ) assume b in Y ; ::_thesis: b <<= x then b <= upper_bound Y by A4, SEQ_4:def_1; hence b <<= x by Th3; ::_thesis: verum end; hence ( Y is_<=_than x & ( for b being Element of R st Y is_<=_than b holds x <<= b ) ) by A11, LATTICE3:def_9; ::_thesis: verum end; end; end; then ex_sup_of Y,R by YELLOW_0:15; hence ex_sup_of X,R by A2, YELLOW_0:50; ::_thesis: verum end; registration cluster non empty interval -> non empty complete interval for RelStr ; coherence for b1 being non empty interval RelStr holds b1 is complete proof let R be non empty interval RelStr ; ::_thesis: R is complete for X being Subset of R holds ex_sup_of X,R by Th8; hence R is complete by YELLOW_0:53; ::_thesis: verum end; end; registration cluster non empty reflexive transitive antisymmetric connected -> distributive for RelStr ; coherence for b1 being Chain holds b1 is distributive proof let C be Chain; ::_thesis: C is distributive for x, y, z being Element of C holds x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) proof let x, y, z be Element of C; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) A1: x <= x ; percases ( ( x <= y & x <= z & y <= z ) or ( x <= y & x <= z & y >= z ) or ( x <= y & x >= z & y <= z ) or ( x <= y & x >= z & y >= z ) or ( x >= y & x <= z & y <= z ) or ( x >= y & x <= z & y >= z ) or ( x >= y & x >= z & y <= z ) or ( x >= y & x >= z & y >= z ) ) by WAYBEL_0:def_29; supposeA2: ( x <= y & x <= z & y <= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) then A3: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24 .= x by A2, YELLOW_0:25 ; (x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A2, YELLOW_0:25 .= x "\/" x by A2, YELLOW_0:25 .= x by A1, YELLOW_0:24 ; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A3; ::_thesis: verum end; supposeA4: ( x <= y & x <= z & y >= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) then A5: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24 .= x by A4, YELLOW_0:25 ; (x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A4, YELLOW_0:25 .= x "\/" x by A4, YELLOW_0:25 .= x by A1, YELLOW_0:24 ; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A5; ::_thesis: verum end; supposeA6: ( x <= y & x >= z & y <= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) then z <= y by YELLOW_0:def_2; then A7: z = y by A6, YELLOW_0:def_3; A8: x "/\" (y "\/" z) = x "/\" z by A6, YELLOW_0:24 .= z by A6, YELLOW_0:25 ; (x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A6, YELLOW_0:25 .= x "\/" z by A6, YELLOW_0:25 .= x by A6, YELLOW_0:24 ; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A6, A7, A8, YELLOW_0:def_3; ::_thesis: verum end; supposeA9: ( x <= y & x >= z & y >= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) then A10: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24 .= x by A9, YELLOW_0:25 ; (x "/\" y) "\/" (x "/\" z) = x "\/" (x "/\" z) by A9, YELLOW_0:25 .= x "\/" z by A9, YELLOW_0:25 .= x by A9, YELLOW_0:24 ; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A10; ::_thesis: verum end; supposeA11: ( x >= y & x <= z & y <= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) then A12: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24 .= x by A11, YELLOW_0:25 ; (x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A11, YELLOW_0:25 .= y "\/" x by A11, YELLOW_0:25 .= x by A11, YELLOW_0:24 ; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A12; ::_thesis: verum end; supposeA13: ( x >= y & x <= z & y >= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) then z >= y by YELLOW_0:def_2; then A14: z = y by A13, YELLOW_0:def_3; A15: x "/\" (y "\/" z) = x "/\" y by A13, YELLOW_0:24 .= y by A13, YELLOW_0:25 ; (x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A13, YELLOW_0:25 .= y "\/" x by A13, YELLOW_0:25 .= x by A13, YELLOW_0:24 ; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A13, A14, A15, YELLOW_0:def_3; ::_thesis: verum end; supposeA16: ( x >= y & x >= z & y <= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) then A17: x "/\" (y "\/" z) = x "/\" z by YELLOW_0:24 .= z by A16, YELLOW_0:25 ; (x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A16, YELLOW_0:25 .= y "\/" z by A16, YELLOW_0:25 .= z by A16, YELLOW_0:24 ; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A17; ::_thesis: verum end; supposeA18: ( x >= y & x >= z & y >= z ) ; ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) then A19: x "/\" (y "\/" z) = x "/\" y by YELLOW_0:24 .= y by A18, YELLOW_0:25 ; (x "/\" y) "\/" (x "/\" z) = y "\/" (x "/\" z) by A18, YELLOW_0:25 .= y "\/" z by A18, YELLOW_0:25 .= y by A18, YELLOW_0:24 ; hence x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) by A19; ::_thesis: verum end; end; end; hence C is distributive by WAYBEL_1:def_3; ::_thesis: verum end; end; registration cluster non empty interval -> non empty Heyting interval for RelStr ; coherence for b1 being non empty interval RelStr holds b1 is Heyting proof let R be non empty interval RelStr ; ::_thesis: R is Heyting thus R is LATTICE ; :: according to WAYBEL_1:def_19 ::_thesis: for b1 being Element of the carrier of R holds b1 "/\" is lower_adjoint let x be Element of R; ::_thesis: x "/\" is lower_adjoint set f = x "/\" ; x "/\" is sups-preserving proof let X be Subset of R; :: according to WAYBEL_0:def_33 ::_thesis: x "/\" preserves_sup_of X assume ex_sup_of X,R ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of (x "/\") .: X,R & "\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R)) ) A1: now__::_thesis:_for_b_being_Element_of_R_st_b_is_>=_than_(x_"/\")_.:_X_holds_ (x_"/\")_._(sup_X)_<<=_b let b be Element of R; ::_thesis: ( b is_>=_than (x "/\") .: X implies (x "/\") . (sup X) <<= b1 ) assume A2: b is_>=_than (x "/\") .: X ; ::_thesis: (x "/\") . (sup X) <<= b1 percases ( x is_>=_than X or not x is_>=_than X ) ; supposeA3: x is_>=_than X ; ::_thesis: (x "/\") . (sup X) <<= b1 b is_>=_than X proof let a be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not a in X or a <<= b ) assume A4: a in X ; ::_thesis: a <<= b then x >>= a by A3, LATTICE3:def_9; then x "/\" a = a by YELLOW_0:25; then A5: a = (x "/\") . a by WAYBEL_1:def_18; (x "/\") . a in (x "/\") .: X by A4, FUNCT_2:35; hence a <<= b by A2, A5, LATTICE3:def_9; ::_thesis: verum end; then A6: b >>= sup X by YELLOW_0:32; x >>= sup X by A3, YELLOW_0:32; then x "/\" (sup X) = sup X by YELLOW_0:25; hence (x "/\") . (sup X) <<= b by A6, WAYBEL_1:def_18; ::_thesis: verum end; suppose not x is_>=_than X ; ::_thesis: (x "/\") . (sup X) <<= b1 then consider a being Element of R such that A7: a in X and A8: not x >>= a by LATTICE3:def_9; A9: x <<= a by A8, WAYBEL_0:def_29; a <<= sup X by A7, YELLOW_2:22; then x <<= sup X by A9, ORDERS_2:3; then x = x "/\" (sup X) by YELLOW_0:25; then A10: x = (x "/\") . (sup X) by WAYBEL_1:def_18; A11: (x "/\") . a in (x "/\") .: X by A7, FUNCT_2:35; x = x "/\" a by A9, YELLOW_0:25 .= (x "/\") . a by WAYBEL_1:def_18 ; hence (x "/\") . (sup X) <<= b by A2, A10, A11, LATTICE3:def_9; ::_thesis: verum end; end; end; thus ex_sup_of (x "/\") .: X,R by Th8; ::_thesis: "\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R)) (x "/\") . (sup X) is_>=_than (x "/\") .: X proof let a be Element of R; :: according to LATTICE3:def_9 ::_thesis: ( not a in (x "/\") .: X or a <<= (x "/\") . (sup X) ) A12: ( (x "/\") . (sup X) = x "/\" (sup X) & x <<= x ) by WAYBEL_1:def_18, YELLOW_0:def_1; assume a in (x "/\") .: X ; ::_thesis: a <<= (x "/\") . (sup X) then consider y being set such that A13: y in the carrier of R and A14: ( y in X & a = (x "/\") . y ) by FUNCT_2:64; reconsider y = y as Element of R by A13; ( y <<= sup X & a = x "/\" y ) by A14, WAYBEL_1:def_18, YELLOW_2:22; hence a <<= (x "/\") . (sup X) by A12, YELLOW_3:2; ::_thesis: verum end; hence "\/" (((x "/\") .: X),R) = (x "/\") . ("\/" (X,R)) by A1, YELLOW_0:30; ::_thesis: verum end; hence x "/\" is lower_adjoint by WAYBEL_1:17; ::_thesis: verum end; end; registration clusterK582(0,1) -> non empty ; coherence not [.0,1.] is empty by MEASURE5:14; end; registration cluster RealPoset [.0,1.] -> strict real interval ; coherence RealPoset [.0,1.] is interval proof the carrier of (RealPoset [.0,1.]) = [.0,1.] by Def3; hence RealPoset [.0,1.] is interval by Def2; ::_thesis: verum end; end; begin theorem Th9: :: LFUZZY_0:9 for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is sup-Semilattice ) holds product J is with_suprema proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is sup-Semilattice ) holds product J is with_suprema let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is sup-Semilattice ) implies product J is with_suprema ) assume A1: for i being Element of I holds J . i is sup-Semilattice ; ::_thesis: product J is with_suprema set IT = product J; for x, y being Element of (product J) ex z being Element of (product J) st ( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds z <= z9 ) ) proof let x, y be Element of (product J); ::_thesis: ex z being Element of (product J) st ( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds z <= z9 ) ) deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = (x . \$1) "\/" (y . \$1); consider z being ManySortedSet of I such that A2: for i being Element of I holds z . i = H1(i) from PBOOLE:sch_5(); A3: for i being Element of I holds z . i is Element of (J . i) proof let i be Element of I; ::_thesis: z . i is Element of (J . i) z . i = (x . i) "\/" (y . i) by A2; hence z . i is Element of (J . i) ; ::_thesis: verum end; dom z = I by PARTFUN1:def_2; then reconsider z = z as Element of (product J) by A3, WAYBEL_3:27; take z ; ::_thesis: ( x <= z & y <= z & ( for z9 being Element of (product J) st x <= z9 & y <= z9 holds z <= z9 ) ) for i being Element of I holds ( x . i <= z . i & y . i <= z . i ) proof let i be Element of I; ::_thesis: ( x . i <= z . i & y . i <= z . i ) ( J . i is antisymmetric with_suprema RelStr & z . i = (x . i) "\/" (y . i) ) by A1, A2; hence ( x . i <= z . i & y . i <= z . i ) by YELLOW_0:22; ::_thesis: verum end; hence ( x <= z & y <= z ) by WAYBEL_3:28; ::_thesis: for z9 being Element of (product J) st x <= z9 & y <= z9 holds z <= z9 let z9 be Element of (product J); ::_thesis: ( x <= z9 & y <= z9 implies z <= z9 ) assume that A4: x <= z9 and A5: y <= z9 ; ::_thesis: z <= z9 for i being Element of I holds z . i <= z9 . i proof let i be Element of I; ::_thesis: z . i <= z9 . i A6: ( z9 . i >= y . i & z . i = (x . i) "\/" (y . i) ) by A2, A5, WAYBEL_3:28; ( J . i is antisymmetric with_suprema RelStr & z9 . i >= x . i ) by A1, A4, WAYBEL_3:28; hence z . i <= z9 . i by A6, YELLOW_0:22; ::_thesis: verum end; hence z <= z9 by WAYBEL_3:28; ::_thesis: verum end; hence product J is with_suprema by LATTICE3:def_10; ::_thesis: verum end; theorem Th10: :: LFUZZY_0:10 for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is Semilattice ) holds product J is with_infima proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is Semilattice ) holds product J is with_infima let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is Semilattice ) implies product J is with_infima ) assume A1: for i being Element of I holds J . i is Semilattice ; ::_thesis: product J is with_infima set IT = product J; for x, y being Element of (product J) ex z being Element of (product J) st ( x >= z & y >= z & ( for z9 being Element of (product J) st x >= z9 & y >= z9 holds z >= z9 ) ) proof let x, y be Element of (product J); ::_thesis: ex z being Element of (product J) st ( x >= z & y >= z & ( for z9 being Element of (product J) st x >= z9 & y >= z9 holds z >= z9 ) ) deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = (x . \$1) "/\" (y . \$1); consider z being ManySortedSet of I such that A2: for i being Element of I holds z . i = H1(i) from PBOOLE:sch_5(); A3: for i being Element of I holds z . i is Element of (J . i) proof let i be Element of I; ::_thesis: z . i is Element of (J . i) z . i = (x . i) "/\" (y . i) by A2; hence z . i is Element of (J . i) ; ::_thesis: verum end; dom z = I by PARTFUN1:def_2; then reconsider z = z as Element of (product J) by A3, WAYBEL_3:27; take z ; ::_thesis: ( x >= z & y >= z & ( for z9 being Element of (product J) st x >= z9 & y >= z9 holds z >= z9 ) ) for i being Element of I holds ( x . i >= z . i & y . i >= z . i ) proof let i be Element of I; ::_thesis: ( x . i >= z . i & y . i >= z . i ) ( J . i is antisymmetric with_infima RelStr & z . i = (x . i) "/\" (y . i) ) by A1, A2; hence ( x . i >= z . i & y . i >= z . i ) by YELLOW_0:23; ::_thesis: verum end; hence ( x >= z & y >= z ) by WAYBEL_3:28; ::_thesis: for z9 being Element of (product J) st x >= z9 & y >= z9 holds z >= z9 let z9 be Element of (product J); ::_thesis: ( x >= z9 & y >= z9 implies z >= z9 ) assume that A4: x >= z9 and A5: y >= z9 ; ::_thesis: z >= z9 for i being Element of I holds z . i >= z9 . i proof let i be Element of I; ::_thesis: z . i >= z9 . i A6: ( z9 . i <= y . i & z . i = (x . i) "/\" (y . i) ) by A2, A5, WAYBEL_3:28; ( J . i is antisymmetric with_infima RelStr & x . i >= z9 . i ) by A1, A4, WAYBEL_3:28; hence z . i >= z9 . i by A6, YELLOW_0:23; ::_thesis: verum end; hence z >= z9 by WAYBEL_3:28; ::_thesis: verum end; hence product J is with_infima by LATTICE3:def_11; ::_thesis: verum end; theorem Th11: :: LFUZZY_0:11 for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is Semilattice ) holds for f, g being Element of (product J) for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i) proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is Semilattice ) holds for f, g being Element of (product J) for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i) let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is Semilattice ) implies for f, g being Element of (product J) for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i) ) assume A1: for i being Element of I holds J . i is Semilattice ; ::_thesis: for f, g being Element of (product J) for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i) let f, g be Element of (product J); ::_thesis: for i being Element of I holds (f "/\" g) . i = (f . i) "/\" (g . i) let i be Element of I; ::_thesis: (f "/\" g) . i = (f . i) "/\" (g . i) A2: J . i is Semilattice by A1; for i being Element of I holds J . i is antisymmetric by A1; then A3: ( product J is antisymmetric & product J is with_infima ) by A1, Th10, WAYBEL_3:30; then g >= f "/\" g by YELLOW_0:23; then A4: g . i >= (f "/\" g) . i by WAYBEL_3:28; A5: (f "/\" g) . i >= (f . i) "/\" (g . i) proof deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = (f . \$1) "/\" (g . \$1); consider z being ManySortedSet of I such that A6: for i being Element of I holds z . i = H1(i) from PBOOLE:sch_5(); A7: for i being Element of I holds z . i is Element of (J . i) proof let i be Element of I; ::_thesis: z . i is Element of (J . i) z . i = (f . i) "/\" (g . i) by A6; hence z . i is Element of (J . i) ; ::_thesis: verum end; dom z = I by PARTFUN1:def_2; then reconsider z = z as Element of (product J) by A7, WAYBEL_3:27; for i being Element of I holds ( z . i <= f . i & z . i <= g . i ) proof let i be Element of I; ::_thesis: ( z . i <= f . i & z . i <= g . i ) ( J . i is antisymmetric with_infima RelStr & z . i = (f . i) "/\" (g . i) ) by A1, A6; hence ( z . i <= f . i & z . i <= g . i ) by YELLOW_0:23; ::_thesis: verum end; then ( z <= f & z <= g ) by WAYBEL_3:28; then A8: f "/\" g >= z by A3, YELLOW_0:23; for i being Element of I holds (f "/\" g) . i >= (f . i) "/\" (g . i) proof let i be Element of I; ::_thesis: (f "/\" g) . i >= (f . i) "/\" (g . i) (f . i) "/\" (g . i) = z . i by A6; hence (f "/\" g) . i >= (f . i) "/\" (g . i) by A8, WAYBEL_3:28; ::_thesis: verum end; hence (f "/\" g) . i >= (f . i) "/\" (g . i) ; ::_thesis: verum end; f >= f "/\" g by A3, YELLOW_0:23; then f . i >= (f "/\" g) . i by WAYBEL_3:28; then (f "/\" g) . i <= (f . i) "/\" (g . i) by A2, A4, YELLOW_0:23; hence (f "/\" g) . i = (f . i) "/\" (g . i) by A2, A5, YELLOW_0:def_3; ::_thesis: verum end; theorem Th12: :: LFUZZY_0:12 for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is sup-Semilattice ) holds for f, g being Element of (product J) for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i) proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is sup-Semilattice ) holds for f, g being Element of (product J) for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i) let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is sup-Semilattice ) implies for f, g being Element of (product J) for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i) ) assume A1: for i being Element of I holds J . i is sup-Semilattice ; ::_thesis: for f, g being Element of (product J) for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i) let f, g be Element of (product J); ::_thesis: for i being Element of I holds (f "\/" g) . i = (f . i) "\/" (g . i) let i be Element of I; ::_thesis: (f "\/" g) . i = (f . i) "\/" (g . i) A2: J . i is sup-Semilattice by A1; for i being Element of I holds J . i is antisymmetric by A1; then A3: ( product J is antisymmetric & product J is with_suprema ) by A1, Th9, WAYBEL_3:30; then g <= f "\/" g by YELLOW_0:22; then A4: g . i <= (f "\/" g) . i by WAYBEL_3:28; A5: (f "\/" g) . i <= (f . i) "\/" (g . i) proof deffunc H1( Element of I) -> Element of the carrier of (J . \$1) = (f . \$1) "\/" (g . \$1); consider z being ManySortedSet of I such that A6: for i being Element of I holds z . i = H1(i) from PBOOLE:sch_5(); A7: for i being Element of I holds z . i is Element of (J . i) proof let i be Element of I; ::_thesis: z . i is Element of (J . i) z . i = (f . i) "\/" (g . i) by A6; hence z . i is Element of (J . i) ; ::_thesis: verum end; dom z = I by PARTFUN1:def_2; then reconsider z = z as Element of (product J) by A7, WAYBEL_3:27; for i being Element of I holds ( z . i >= f . i & z . i >= g . i ) proof let i be Element of I; ::_thesis: ( z . i >= f . i & z . i >= g . i ) ( J . i is antisymmetric with_suprema RelStr & z . i = (f . i) "\/" (g . i) ) by A1, A6; hence ( z . i >= f . i & z . i >= g . i ) by YELLOW_0:22; ::_thesis: verum end; then ( z >= f & z >= g ) by WAYBEL_3:28; then A8: f "\/" g <= z by A3, YELLOW_0:22; for i being Element of I holds (f "\/" g) . i <= (f . i) "\/" (g . i) proof let i be Element of I; ::_thesis: (f "\/" g) . i <= (f . i) "\/" (g . i) (f . i) "\/" (g . i) = z . i by A6; hence (f "\/" g) . i <= (f . i) "\/" (g . i) by A8, WAYBEL_3:28; ::_thesis: verum end; hence (f "\/" g) . i <= (f . i) "\/" (g . i) ; ::_thesis: verum end; f <= f "\/" g by A3, YELLOW_0:22; then f . i <= (f "\/" g) . i by WAYBEL_3:28; then (f "\/" g) . i >= (f . i) "\/" (g . i) by A2, A4, YELLOW_0:22; hence (f "\/" g) . i = (f . i) "\/" (g . i) by A2, A5, YELLOW_0:def_3; ::_thesis: verum end; theorem Th13: :: LFUZZY_0:13 for I being non empty set for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete Heyting LATTICE ) holds ( product J is complete & product J is Heyting ) proof let I be non empty set ; ::_thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I st ( for i being Element of I holds J . i is complete Heyting LATTICE ) holds ( product J is complete & product J is Heyting ) let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; ::_thesis: ( ( for i being Element of I holds J . i is complete Heyting LATTICE ) implies ( product J is complete & product J is Heyting ) ) assume A1: for i being Element of I holds J . i is complete Heyting LATTICE ; ::_thesis: ( product J is complete & product J is Heyting ) A2: for i being Element of I holds J . i is complete LATTICE by A1; set H = product J; reconsider H = product J as complete LATTICE by A2, WAYBEL_3:31; H = H ; hence ( product J is complete & product J is LATTICE ) ; :: according to WAYBEL_1:def_19 ::_thesis: for b1 being Element of the carrier of (product J) holds b1 "/\" is lower_adjoint let f be Element of (product J); ::_thesis: f "/\" is lower_adjoint reconsider g = f as Element of H ; reconsider F = f "/\" as Function of H,H ; A3: for i being Element of I holds J . i is Semilattice by A1; F is sups-preserving proof let X be Subset of H; :: according to WAYBEL_0:def_33 ::_thesis: F preserves_sup_of X reconsider Y = F .: X, X9 = X as Subset of (product J) ; reconsider sX = sup X as Element of (product J) ; assume ex_sup_of X,H ; :: according to WAYBEL_0:def_31 ::_thesis: ( ex_sup_of F .: X,H & "\/" ((F .: X),H) = F . ("\/" (X,H)) ) thus ex_sup_of F .: X,H by YELLOW_0:17; ::_thesis: "\/" ((F .: X),H) = F . ("\/" (X,H)) reconsider f1 = sup (F .: X), f2 = F . (sup X) as Element of (product J) ; A4: now__::_thesis:_for_x_being_set_st_x_in_dom_f1_holds_ f1_._x_=_f2_._x let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x ) assume x in dom f1 ; ::_thesis: f1 . x = f2 . x then reconsider i = x as Element of I by WAYBEL_3:27; A5: J . i is complete Heyting LATTICE by A1; then A6: ex_sup_of pi (X9,i),J . i by YELLOW_0:17; A7: ((f . i) "/\") .: (pi (X9,i)) c= pi (Y,i) proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in ((f . i) "/\") .: (pi (X9,i)) or b in pi (Y,i) ) assume b in ((f . i) "/\") .: (pi (X9,i)) ; ::_thesis: b in pi (Y,i) then consider f4 being set such that f4 in dom ((f . i) "/\") and A8: f4 in pi (X9,i) and A9: b = ((f . i) "/\") . f4 by FUNCT_1:def_6; consider f5 being Function such that A10: f5 in X9 and A11: f4 = f5 . i by A8, CARD_3:def_6; reconsider f5 = f5 as Element of (product J) by A10; f "/\" f5 = (f "/\") . f5 by WAYBEL_1:def_18; then A12: f "/\" f5 in (f "/\") .: X by A10, FUNCT_2:35; ((f . i) "/\") . f4 = (f . i) "/\" (f5 . i) by A11, WAYBEL_1:def_18 .= (f "/\" f5) . i by A3, Th11 ; hence b in pi (Y,i) by A9, A12, CARD_3:def_6; ::_thesis: verum end; pi (Y,i) c= ((f . i) "/\") .: (pi (X9,i)) proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in pi (Y,i) or a in ((f . i) "/\") .: (pi (X9,i)) ) assume a in pi (Y,i) ; ::_thesis: a in ((f . i) "/\") .: (pi (X9,i)) then consider f3 being Function such that A13: f3 in Y and A14: a = f3 . i by CARD_3:def_6; reconsider f3 = f3 as Element of (product J) by A13; consider h being set such that A15: h in dom F and A16: h in X and A17: f3 = F . h by A13, FUNCT_1:def_6; reconsider h = h as Element of (product J) by A15; A18: h . i in pi (X9,i) by A16, CARD_3:def_6; f3 . i = (f "/\" h) . i by A17, WAYBEL_1:def_18 .= (f . i) "/\" (h . i) by A3, Th11 .= ((f . i) "/\") . (h . i) by WAYBEL_1:def_18 ; hence a in ((f . i) "/\") .: (pi (X9,i)) by A14, A18, FUNCT_2:35; ::_thesis: verum end; then A19: pi (Y,i) = ((f . i) "/\") .: (pi (X9,i)) by A7, XBOOLE_0:def_10; (f . i) "/\" is lower_adjoint by A5, WAYBEL_1:def_19; then A20: (f . i) "/\" preserves_sup_of pi (X9,i) by A5, WAYBEL_0:def_33; f2 = g "/\" (sup X) by WAYBEL_1:def_18; then f2 . i = (f . i) "/\" (sX . i) by A3, Th11 .= (f . i) "/\" (sup (pi (X9,i))) by A2, WAYBEL_3:32 .= ((f . i) "/\") . (sup (pi (X9,i))) by WAYBEL_1:def_18 .= sup (((f . i) "/\") .: (pi (X9,i))) by A20, A6, WAYBEL_0:def_31 ; hence f1 . x = f2 . x by A2, A19, WAYBEL_3:32; ::_thesis: verum end; ( dom f1 = I & dom f2 = I ) by WAYBEL_3:27; hence "\/" ((F .: X),H) = F . ("\/" (X,H)) by A4, FUNCT_1:2; ::_thesis: verum end; hence f "/\" is lower_adjoint by WAYBEL_1:17; ::_thesis: verum end; registration let A be non empty set ; let R be complete Heyting LATTICE; clusterR |^ A -> Heyting ; coherence R |^ A is Heyting proof for i being Element of A holds (A --> R) . i is complete Heyting LATTICE by FUNCOP_1:7; then ( product (A --> R) is complete & product (A --> R) is Heyting ) by Th13; hence R |^ A is Heyting by YELLOW_1:def_5; ::_thesis: verum end; end; begin definition let A be non empty set ; func FuzzyLattice A -> complete Heyting LATTICE equals :: LFUZZY_0:def 4 (RealPoset [.0,1.]) |^ A; coherence (RealPoset [.0,1.]) |^ A is complete Heyting LATTICE ; end; :: deftheorem defines FuzzyLattice LFUZZY_0:def_4_:_ for A being non empty set holds FuzzyLattice A = (RealPoset [.0,1.]) |^ A; theorem Th14: :: LFUZZY_0:14 for A being non empty set holds the carrier of (FuzzyLattice A) = Funcs (A,[.0,1.]) proof let A be non empty set ; ::_thesis: the carrier of (FuzzyLattice A) = Funcs (A,[.0,1.]) thus the carrier of (FuzzyLattice A) = Funcs (A, the carrier of (RealPoset [.0,1.])) by YELLOW_1:28 .= Funcs (A,[.0,1.]) by Def3 ; ::_thesis: verum end; Lm1: for A being non empty set holds FuzzyLattice A is constituted-Functions proof let A be non empty set ; ::_thesis: FuzzyLattice A is constituted-Functions for a being Element of (FuzzyLattice A) holds a is Function proof let a be Element of (FuzzyLattice A); ::_thesis: a is Function a in the carrier of (FuzzyLattice A) ; then a in Funcs (A,[.0,1.]) by Th14; then ex f being Function st ( a = f & dom f = A & rng f c= [.0,1.] ) by FUNCT_2:def_2; hence a is Function ; ::_thesis: verum end; hence FuzzyLattice A is constituted-Functions by MONOID_0:def_1; ::_thesis: verum end; registration let A be non empty set ; cluster FuzzyLattice A -> complete constituted-Functions Heyting ; coherence FuzzyLattice A is constituted-Functions by Lm1; end; theorem Th15: :: LFUZZY_0:15 for R being complete Heyting LATTICE for X being Subset of R for y being Element of R holds ("\/" (X,R)) "/\" y = "\/" ( { (x "/\" y) where x is Element of R : x in X } ,R) proof let R be complete Heyting LATTICE; ::_thesis: for X being Subset of R for y being Element of R holds ("\/" (X,R)) "/\" y = "\/" ( { (x "/\" y) where x is Element of R : x in X } ,R) let X be Subset of R; ::_thesis: for y being Element of R holds ("\/" (X,R)) "/\" y = "\/" ( { (x "/\" y) where x is Element of R : x in X } ,R) let y be Element of R; ::_thesis: ("\/" (X,R)) "/\" y = "\/" ( { (x "/\" y) where x is Element of R : x in X } ,R) set Z = { (y "/\" x) where x is Element of R : x in X } ; set W = { (x "/\" y) where x is Element of R : x in X } ; A1: { (x "/\" y) where x is Element of R : x in X } c= { (y "/\" x) where x is Element of R : x in X } proof let w be set ; :: according to TARSKI:def_3 ::_thesis: ( not w in { (x "/\" y) where x is Element of R : x in X } or w in { (y "/\" x) where x is Element of R : x in X } ) assume w in { (x "/\" y) where x is Element of R : x in X } ; ::_thesis: w in { (y "/\" x) where x is Element of R : x in X } then ex x being Element of R st ( w = x "/\" y & x in X ) ; hence w in { (y "/\" x) where x is Element of R : x in X } ; ::_thesis: verum end; { (y "/\" x) where x is Element of R : x in X } c= { (x "/\" y) where x is Element of R : x in X } proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { (y "/\" x) where x is Element of R : x in X } or z in { (x "/\" y) where x is Element of R : x in X } ) assume z in { (y "/\" x) where x is Element of R : x in X } ; ::_thesis: z in { (x "/\" y) where x is Element of R : x in X } then ex x being Element of R st ( z = y "/\" x & x in X ) ; hence z in { (x "/\" y) where x is Element of R : x in X } ; ::_thesis: verum end; then ( ( for z being Element of R holds ( z "/\" is lower_adjoint & ex_sup_of X,R ) ) & { (y "/\" x) where x is Element of R : x in X } = { (x "/\" y) where x is Element of R : x in X } ) by A1, WAYBEL_1:def_19, XBOOLE_0:def_10, YELLOW_0:17; hence ("\/" (X,R)) "/\" y = "\/" ( { (x "/\" y) where x is Element of R : x in X } ,R) by WAYBEL_1:63; ::_thesis: verum end; Lm2: for X being non empty set for a being Element of (FuzzyLattice X) holds a is Membership_Func of X proof let X be non empty set ; ::_thesis: for a being Element of (FuzzyLattice X) holds a is Membership_Func of X let a be Element of (FuzzyLattice X); ::_thesis: a is Membership_Func of X a in the carrier of (FuzzyLattice X) ; then a in Funcs (X,[.0,1.]) by Th14; then A1: ex f being Function st ( a = f & dom f = X & rng f c= [.0,1.] ) by FUNCT_2:def_2; then reconsider a = a as PartFunc of X,[.0,1.] by RELSET_1:4; reconsider a = a as PartFunc of X,REAL by RELSET_1:7; a is Function of X,REAL by A1, FUNCT_2:def_1; hence a is Membership_Func of X ; ::_thesis: verum end; definition let X be non empty set ; let a be Element of (FuzzyLattice X); func @ a -> Membership_Func of X equals :: LFUZZY_0:def 5 a; coherence a is Membership_Func of X by Lm2; end; :: deftheorem defines @ LFUZZY_0:def_5_:_ for X being non empty set for a being Element of (FuzzyLattice X) holds @ a = a; Lm3: for X being non empty set for f being Membership_Func of X holds f is Element of (FuzzyLattice X) proof let X be non empty set ; ::_thesis: for f being Membership_Func of X holds f is Element of (FuzzyLattice X) let f be Membership_Func of X; ::_thesis: f is Element of (FuzzyLattice X) ( dom f = X & rng f c= [.0,1.] ) by FUNCT_2:def_1, RELAT_1:def_19; then f in Funcs (X,[.0,1.]) by FUNCT_2:def_2; hence f is Element of (FuzzyLattice X) by Th14; ::_thesis: verum end; definition let X be non empty set ; let f be Membership_Func of X; func(X,f) @ -> Element of (FuzzyLattice X) equals :: LFUZZY_0:def 6 f; coherence f is Element of (FuzzyLattice X) by Lm3; end; :: deftheorem defines @ LFUZZY_0:def_6_:_ for X being non empty set for f being Membership_Func of X holds (X,f) @ = f; definition let X be non empty set ; let f be Membership_Func of X; let x be Element of X; :: original: . redefine funcf . x -> Element of (RealPoset [.0,1.]); coherence f . x is Element of (RealPoset [.0,1.]) proof ( 0 <= f . x & f . x <= 1 ) by FUZZY_2:1; then f . x in [.0,1.] by XXREAL_1:1; hence f . x is Element of (RealPoset [.0,1.]) by Def3; ::_thesis: verum end; end; definition let X, Y be non empty set ; let f be RMembership_Func of X,Y; let x be Element of X; let y be Element of Y; :: original: . redefine funcf . (x,y) -> Element of (RealPoset [.0,1.]); coherence f . (x,y) is Element of (RealPoset [.0,1.]) proof f . [x,y] is Element of (RealPoset [.0,1.]) ; hence f . (x,y) is Element of (RealPoset [.0,1.]) ; ::_thesis: verum end; end; definition let X be non empty set ; let f be Element of (FuzzyLattice X); let x be Element of X; :: original: . redefine funcf . x -> Element of (RealPoset [.0,1.]); coherence f . x is Element of (RealPoset [.0,1.]) proof 0 <= (@ f) . x by FUZZY_2:1; hence f . x is Element of (RealPoset [.0,1.]) ; ::_thesis: verum end; end; theorem Th16: :: LFUZZY_0:16 for C being non empty set for f, g being Membership_Func of C holds ( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ ) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds ( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ ) let f, g be Membership_Func of C; ::_thesis: ( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ ) A1: (RealPoset [.0,1.]) |^ C = product (C --> (RealPoset [.0,1.])) by YELLOW_1:def_5; A2: ( ( for c being Element of C holds f . c <= g . c ) implies (C,f) @ <<= (C,g) @ ) proof set f9 = (C,f) @ ; set g9 = (C,g) @ ; reconsider f9 = (C,f) @ , g9 = (C,g) @ as Element of (product (C --> (RealPoset [.0,1.]))) by YELLOW_1:def_5; assume A3: for c being Element of C holds f . c <= g . c ; ::_thesis: (C,f) @ <<= (C,g) @ for c being Element of C holds f9 . c <<= g9 . c proof let c be Element of C; ::_thesis: f9 . c <<= g9 . c set f1 = f . c; set g1 = g . c; ( (C --> (RealPoset [.0,1.])) . c = RealPoset [.0,1.] & f . c <= g . c ) by A3, FUNCOP_1:7; hence f9 . c <<= g9 . c by Th3; ::_thesis: verum end; hence (C,f) @ <<= (C,g) @ by A1, WAYBEL_3:28; ::_thesis: verum end; ( (C,f) @ <<= (C,g) @ implies for c being Element of C holds f . c <= g . c ) proof reconsider ff = (C,f) @ , gg = (C,g) @ as Element of (product (C --> (RealPoset [.0,1.]))) by YELLOW_1:def_5; assume A4: (C,f) @ <<= (C,g) @ ; ::_thesis: for c being Element of C holds f . c <= g . c let c be Element of C; ::_thesis: f . c <= g . c ( (C --> (RealPoset [.0,1.])) . c = RealPoset [.0,1.] & ff . c <<= gg . c ) by A1, A4, FUNCOP_1:7, WAYBEL_3:28; hence f . c <= g . c by Th3; ::_thesis: verum end; hence ( ( for c being Element of C holds f . c <= g . c ) iff (C,f) @ <<= (C,g) @ ) by A2; ::_thesis: verum end; theorem :: LFUZZY_0:17 for C being non empty set for s, t being Element of (FuzzyLattice C) holds ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c ) proof let C be non empty set ; ::_thesis: for s, t being Element of (FuzzyLattice C) holds ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c ) let s, t be Element of (FuzzyLattice C); ::_thesis: ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c ) ( (C,(@ s)) @ = s & (C,(@ t)) @ = t ) ; hence ( s <<= t iff for c being Element of C holds (@ s) . c <= (@ t) . c ) by Th16; ::_thesis: verum end; theorem Th18: :: LFUZZY_0:18 for C being non empty set for f, g being Membership_Func of C holds max (f,g) = ((C,f) @) "\/" ((C,g) @) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds max (f,g) = ((C,f) @) "\/" ((C,g) @) let f, g be Membership_Func of C; ::_thesis: max (f,g) = ((C,f) @) "\/" ((C,g) @) set fg = ((C,f) @) "\/" ((C,g) @); set R = RealPoset [.0,1.]; set J = C --> (RealPoset [.0,1.]); A1: (RealPoset [.0,1.]) |^ C = product (C --> (RealPoset [.0,1.])) by YELLOW_1:def_5; now__::_thesis:_for_c_being_Element_of_C_holds_(@_(((C,f)_@)_"\/"_((C,g)_@)))_._c_=_max_((f_._c),(g_._c)) let c be Element of C; ::_thesis: (@ (((C,f) @) "\/" ((C,g) @))) . c = max ((f . c),(g . c)) ( ( for c being Element of C holds (C --> (RealPoset [.0,1.])) . c is sup-Semilattice ) & (C --> (RealPoset [.0,1.])) . c = RealPoset [.0,1.] ) by FUNCOP_1:7; hence (@ (((C,f) @) "\/" ((C,g) @))) . c = (((C,f) @) . c) "\/" (((C,g) @) . c) by A1, Th12 .= max ((f . c),(g . c)) ; ::_thesis: verum end; hence max (f,g) = ((C,f) @) "\/" ((C,g) @) by FUZZY_1:def_4; ::_thesis: verum end; theorem :: LFUZZY_0:19 for C being non empty set for s, t being Element of (FuzzyLattice C) holds s "\/" t = max ((@ s),(@ t)) proof let C be non empty set ; ::_thesis: for s, t being Element of (FuzzyLattice C) holds s "\/" t = max ((@ s),(@ t)) let s, t be Element of (FuzzyLattice C); ::_thesis: s "\/" t = max ((@ s),(@ t)) ( (C,(@ s)) @ = s & (C,(@ t)) @ = t ) ; hence s "\/" t = max ((@ s),(@ t)) by Th18; ::_thesis: verum end; theorem Th20: :: LFUZZY_0:20 for C being non empty set for f, g being Membership_Func of C holds min (f,g) = ((C,f) @) "/\" ((C,g) @) proof let C be non empty set ; ::_thesis: for f, g being Membership_Func of C holds min (f,g) = ((C,f) @) "/\" ((C,g) @) let f, g be Membership_Func of C; ::_thesis: min (f,g) = ((C,f) @) "/\" ((C,g) @) set fg = ((C,f) @) "/\" ((C,g) @); set R = RealPoset [.0,1.]; set J = C --> (RealPoset [.0,1.]); A1: (RealPoset [.0,1.]) |^ C = product (C --> (RealPoset [.0,1.])) by YELLOW_1:def_5; now__::_thesis:_for_c_being_Element_of_C_holds_(@_(((C,f)_@)_"/\"_((C,g)_@)))_._c_=_min_((f_._c),(g_._c)) let c be Element of C; ::_thesis: (@ (((C,f) @) "/\" ((C,g) @))) . c = min ((f . c),(g . c)) ( ( for c being Element of C holds (C --> (RealPoset [.0,1.])) . c is Semilattice ) & (C --> (RealPoset [.0,1.])) . c = RealPoset [.0,1.] ) by FUNCOP_1:7; hence (@ (((C,f) @) "/\" ((C,g) @))) . c = (((C,f) @) . c) "/\" (((C,g) @) . c) by A1, Th11 .= min ((f . c),(g . c)) ; ::_thesis: verum end; hence min (f,g) = ((C,f) @) "/\" ((C,g) @) by FUZZY_1:def_3; ::_thesis: verum end; theorem :: LFUZZY_0:21 for C being non empty set for s, t being Element of (FuzzyLattice C) holds s "/\" t = min ((@ s),(@ t)) proof let C be non empty set ; ::_thesis: for s, t being Element of (FuzzyLattice C) holds s "/\" t = min ((@ s),(@ t)) let s, t be Element of (FuzzyLattice C); ::_thesis: s "/\" t = min ((@ s),(@ t)) ( (C,(@ s)) @ = s & (C,(@ t)) @ = t ) ; hence s "/\" t = min ((@ s),(@ t)) by Th20; ::_thesis: verum end; begin scheme :: LFUZZY_0:sch 1 SupDistributivity{ F1() -> complete LATTICE, F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F1(), P1[ set ], P2[ set ] } : "\/" ( { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,F1()) = "\/" ( { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,F1()) proof defpred S1[ set ] means ex x being Element of F2() st ( P1[x] & ( for a being set holds ( a in \$1 iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) ) ); A1: "\/" ( { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ,F1()) = "\/" ((union { A where A is Subset of F1() : S1[A] } ),F1()) from YELLOW_3:sch_5(); A2: { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } c= union { A where A is Subset of F1() : S1[A] } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } or a in union { A where A is Subset of F1() : S1[A] } ) assume a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ; ::_thesis: a in union { A where A is Subset of F1() : S1[A] } then consider x being Element of F2(), y being Element of F3() such that A3: a = F4(x,y) and A4: P1[x] and A5: P2[y] ; set A1 = { F4(x,y9) where y9 is Element of F3() : P2[y9] } ; { F4(x,y9) where y9 is Element of F3() : P2[y9] } c= the carrier of F1() proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { F4(x,y9) where y9 is Element of F3() : P2[y9] } or b in the carrier of F1() ) assume b in { F4(x,y9) where y9 is Element of F3() : P2[y9] } ; ::_thesis: b in the carrier of F1() then ex y9 being Element of F3() st ( b = F4(x,y9) & P2[y9] ) ; hence b in the carrier of F1() ; ::_thesis: verum end; then reconsider A1 = { F4(x,y9) where y9 is Element of F3() : P2[y9] } as Subset of F1() ; S1[A1] proof take x ; ::_thesis: ( P1[x] & ( for a being set holds ( a in A1 iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) ) ) thus P1[x] by A4; ::_thesis: for a being set holds ( a in A1 iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) let a be set ; ::_thesis: ( a in A1 iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) thus ( a in A1 iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) ; ::_thesis: verum end; then A6: A1 in { A where A is Subset of F1() : S1[A] } ; a in A1 by A3, A5; hence a in union { A where A is Subset of F1() : S1[A] } by A6, TARSKI:def_4; ::_thesis: verum end; A7: { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } c= { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } or a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ) assume a in { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ; ::_thesis: a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } then consider x being Element of F2() such that A8: a = "\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1()) and A9: P1[x] ; ex A1 being Subset of F1() st ( a = "\/" (A1,F1()) & S1[A1] ) proof set A2 = { F4(x,y) where y is Element of F3() : P2[y] } ; { F4(x,y) where y is Element of F3() : P2[y] } c= the carrier of F1() proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { F4(x,y) where y is Element of F3() : P2[y] } or b in the carrier of F1() ) assume b in { F4(x,y) where y is Element of F3() : P2[y] } ; ::_thesis: b in the carrier of F1() then ex y being Element of F3() st ( b = F4(x,y) & P2[y] ) ; hence b in the carrier of F1() ; ::_thesis: verum end; then reconsider A1 = { F4(x,y) where y is Element of F3() : P2[y] } as Subset of F1() ; S1[A1] proof take x ; ::_thesis: ( P1[x] & ( for a being set holds ( a in A1 iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) ) ) thus P1[x] by A9; ::_thesis: for a being set holds ( a in A1 iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) thus for a being set holds ( a in A1 iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) ; ::_thesis: verum end; hence ex A1 being Subset of F1() st ( a = "\/" (A1,F1()) & S1[A1] ) by A8; ::_thesis: verum end; hence a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ; ::_thesis: verum end; A10: { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } c= { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } or a in { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ) assume a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ; ::_thesis: a in { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } then consider A1 being Subset of F1() such that A11: a = "\/" (A1,F1()) and A12: S1[A1] ; consider x being Element of F2() such that A13: P1[x] and A14: for a being set holds ( a in A1 iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) by A12; now__::_thesis:_for_a_being_set_holds_ (_a_in_A1_iff_a_in__{__F4(x,y)_where_y_is_Element_of_F3()_:_P2[y]__}__) let a be set ; ::_thesis: ( a in A1 iff a in { F4(x,y) where y is Element of F3() : P2[y] } ) ( a in { F4(x,y) where y is Element of F3() : P2[y] } iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) ; hence ( a in A1 iff a in { F4(x,y) where y is Element of F3() : P2[y] } ) by A14; ::_thesis: verum end; then A1 = { F4(x,y) where y is Element of F3() : P2[y] } by TARSKI:1; hence a in { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } by A11, A13; ::_thesis: verum end; union { A where A is Subset of F1() : S1[A] } c= { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { A where A is Subset of F1() : S1[A] } or a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ) assume a in union { A where A is Subset of F1() : S1[A] } ; ::_thesis: a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } then consider A1 being set such that A15: a in A1 and A16: A1 in { A where A is Subset of F1() : S1[A] } by TARSKI:def_4; consider A2 being Subset of F1() such that A17: A1 = A2 and A18: S1[A2] by A16; consider x being Element of F2() such that A19: P1[x] and A20: for a being set holds ( a in A2 iff ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) ) by A18; ex y being Element of F3() st ( a = F4(x,y) & P2[y] ) by A15, A17, A20; hence a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } by A19; ::_thesis: verum end; then union { A where A is Subset of F1() : S1[A] } = { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } by A2, XBOOLE_0:def_10; hence "\/" ( { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,F1()) = "\/" ( { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,F1()) by A1, A10, A7, XBOOLE_0:def_10; ::_thesis: verum end; scheme :: LFUZZY_0:sch 2 SupDistributivity9{ F1() -> complete LATTICE, F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F1(), P1[ set ], P2[ set ] } : "\/" ( { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } ,F1()) = "\/" ( { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,F1()) proof defpred S1[ set ] means ex y being Element of F3() st ( P2[y] & ( for a being set holds ( a in \$1 iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) ) ); A1: "\/" ( { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ,F1()) = "\/" ((union { A where A is Subset of F1() : S1[A] } ),F1()) from YELLOW_3:sch_5(); A2: { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } c= union { A where A is Subset of F1() : S1[A] } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } or a in union { A where A is Subset of F1() : S1[A] } ) assume a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ; ::_thesis: a in union { A where A is Subset of F1() : S1[A] } then consider x being Element of F2(), y being Element of F3() such that A3: ( a = F4(x,y) & P1[x] ) and A4: P2[y] ; set A1 = { F4(x9,y) where x9 is Element of F2() : P1[x9] } ; { F4(x9,y) where x9 is Element of F2() : P1[x9] } c= the carrier of F1() proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { F4(x9,y) where x9 is Element of F2() : P1[x9] } or b in the carrier of F1() ) assume b in { F4(x9,y) where x9 is Element of F2() : P1[x9] } ; ::_thesis: b in the carrier of F1() then ex x9 being Element of F2() st ( b = F4(x9,y) & P1[x9] ) ; hence b in the carrier of F1() ; ::_thesis: verum end; then reconsider A1 = { F4(x9,y) where x9 is Element of F2() : P1[x9] } as Subset of F1() ; S1[A1] proof take y ; ::_thesis: ( P2[y] & ( for a being set holds ( a in A1 iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) ) ) thus P2[y] by A4; ::_thesis: for a being set holds ( a in A1 iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) let a be set ; ::_thesis: ( a in A1 iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) thus ( a in A1 iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) ; ::_thesis: verum end; then A5: A1 in { A where A is Subset of F1() : S1[A] } ; a in A1 by A3; hence a in union { A where A is Subset of F1() : S1[A] } by A5, TARSKI:def_4; ::_thesis: verum end; A6: { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } c= { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } or a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ) assume a in { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } ; ::_thesis: a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } then consider y being Element of F3() such that A7: a = "\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1()) and A8: P2[y] ; ex A1 being Subset of F1() st ( a = "\/" (A1,F1()) & S1[A1] ) proof set A2 = { F4(x,y) where x is Element of F2() : P1[x] } ; { F4(x,y) where x is Element of F2() : P1[x] } c= the carrier of F1() proof let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { F4(x,y) where x is Element of F2() : P1[x] } or b in the carrier of F1() ) assume b in { F4(x,y) where x is Element of F2() : P1[x] } ; ::_thesis: b in the carrier of F1() then ex x being Element of F2() st ( b = F4(x,y) & P1[x] ) ; hence b in the carrier of F1() ; ::_thesis: verum end; then reconsider A1 = { F4(x,y) where x is Element of F2() : P1[x] } as Subset of F1() ; S1[A1] proof take y ; ::_thesis: ( P2[y] & ( for a being set holds ( a in A1 iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) ) ) thus P2[y] by A8; ::_thesis: for a being set holds ( a in A1 iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) thus for a being set holds ( a in A1 iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) ; ::_thesis: verum end; hence ex A1 being Subset of F1() st ( a = "\/" (A1,F1()) & S1[A1] ) by A7; ::_thesis: verum end; hence a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ; ::_thesis: verum end; A9: { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } c= { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } or a in { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } ) assume a in { ("\/" (A,F1())) where A is Subset of F1() : S1[A] } ; ::_thesis: a in { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } then consider A1 being Subset of F1() such that A10: a = "\/" (A1,F1()) and A11: S1[A1] ; consider y being Element of F3() such that A12: P2[y] and A13: for a being set holds ( a in A1 iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) by A11; now__::_thesis:_for_a_being_set_holds_ (_a_in_A1_iff_a_in__{__F4(x,y)_where_x_is_Element_of_F2()_:_P1[x]__}__) let a be set ; ::_thesis: ( a in A1 iff a in { F4(x,y) where x is Element of F2() : P1[x] } ) ( a in { F4(x,y) where x is Element of F2() : P1[x] } iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) ; hence ( a in A1 iff a in { F4(x,y) where x is Element of F2() : P1[x] } ) by A13; ::_thesis: verum end; then A1 = { F4(x,y) where x is Element of F2() : P1[x] } by TARSKI:1; hence a in { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } by A10, A12; ::_thesis: verum end; union { A where A is Subset of F1() : S1[A] } c= { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } proof let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in union { A where A is Subset of F1() : S1[A] } or a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ) assume a in union { A where A is Subset of F1() : S1[A] } ; ::_thesis: a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } then consider A1 being set such that A14: a in A1 and A15: A1 in { A where A is Subset of F1() : S1[A] } by TARSKI:def_4; consider A2 being Subset of F1() such that A16: A1 = A2 and A17: S1[A2] by A15; consider y being Element of F3() such that A18: P2[y] and A19: for a being set holds ( a in A2 iff ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) ) by A17; ex x being Element of F2() st ( a = F4(x,y) & P1[x] ) by A14, A16, A19; hence a in { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } by A18; ::_thesis: verum end; then union { A where A is Subset of F1() : S1[A] } = { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } by A2, XBOOLE_0:def_10; hence "\/" ( { ("\/" ( { F4(x,y) where x is Element of F2() : P1[x] } ,F1())) where y is Element of F3() : P2[y] } ,F1()) = "\/" ( { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,F1()) by A1, A9, A6, XBOOLE_0:def_10; ::_thesis: verum end; scheme :: LFUZZY_0:sch 3 FraenkelF9R9{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , F4( set , set ) -> set , P1[ set , set ] } : { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] } provided A1: for u being Element of F1() for v being Element of F2() st P1[u,v] holds F3(u,v) = F4(u,v) proof set A = { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } ; set C = { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } ; for a being set holds ( a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } iff a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } ) proof let a be set ; ::_thesis: ( a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } iff a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } ) hereby ::_thesis: ( a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } implies a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } ) assume a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } ; ::_thesis: a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } then consider u being Element of F1(), v being Element of F2() such that A2: a = F3(u,v) and A3: P1[u,v] ; a = F4(u,v) by A1, A2, A3; hence a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } by A3; ::_thesis: verum end; assume a in { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } ; ::_thesis: a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } then consider u being Element of F1(), v being Element of F2() such that A4: a = F4(u,v) and A5: P1[u,v] ; a = F3(u,v) by A1, A4, A5; hence a in { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } by A5; ::_thesis: verum end; hence { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P1[u2,v2] } by TARSKI:1; ::_thesis: verum end; scheme :: LFUZZY_0:sch 4 FraenkelF699R{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , F4( set , set ) -> set , P1[ set , set ], P2[ set , set ] } : { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } provided A1: for u being Element of F1() for v being Element of F2() holds ( P1[u,v] iff P2[u,v] ) and A2: for u being Element of F1() for v being Element of F2() st P1[u,v] holds F3(u,v) = F4(u,v) proof set A = { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } ; set B = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } ; set C = { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } ; A3: { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } from FRAENKEL:sch_4(A1); { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u3,v3) where u3 is Element of F1(), v3 is Element of F2() : P1[u3,v3] } from LFUZZY_0:sch_3(A2); hence { F3(u1,v1) where u1 is Element of F1(), v1 is Element of F2() : P1[u1,v1] } = { F4(u2,v2) where u2 is Element of F1(), v2 is Element of F2() : P2[u2,v2] } by A3; ::_thesis: verum end; scheme :: LFUZZY_0:sch 5 SupCommutativity{ F1() -> complete LATTICE, F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F1(), F5( set , set ) -> Element of F1(), P1[ set ], P2[ set ] } : "\/" ( { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,F1()) = "\/" ( { ("\/" ( { F5(x9,y9) where x9 is Element of F2() : P1[x9] } ,F1())) where y9 is Element of F3() : P2[y9] } ,F1()) provided A1: for x being Element of F2() for y being Element of F3() st P1[x] & P2[y] holds F4(x,y) = F5(x,y) proof defpred S1[ set , set ] means ( P1[\$1] & P2[\$2] ); A2: for x being Element of F2() for y being Element of F3() holds ( S1[x,y] iff S1[x,y] ) ; A3: for x being Element of F2() for y being Element of F3() st S1[x,y] holds F4(x,y) = F5(x,y) by A1; A4: { F4(x9,y9) where x9 is Element of F2(), y9 is Element of F3() : S1[x9,y9] } = { F5(x,y) where x is Element of F2(), y is Element of F3() : S1[x,y] } from LFUZZY_0:sch_4(A2, A3); A5: "\/" ( { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,F1()) = "\/" ( { F4(x,y) where x is Element of F2(), y is Element of F3() : ( P1[x] & P2[y] ) } ,F1()) from LFUZZY_0:sch_1(); "\/" ( { ("\/" ( { F5(x9,y9) where x9 is Element of F2() : P1[x9] } ,F1())) where y9 is Element of F3() : P2[y9] } ,F1()) = "\/" ( { F5(x9,y9) where x9 is Element of F2(), y9 is Element of F3() : ( P1[x9] & P2[y9] ) } ,F1()) from LFUZZY_0:sch_2() .= "\/" ( { F4(x9,y9) where x9 is Element of F2(), y9 is Element of F3() : ( P1[x9] & P2[y9] ) } ,F1()) by A4 ; hence "\/" ( { ("\/" ( { F4(x,y) where y is Element of F3() : P2[y] } ,F1())) where x is Element of F2() : P1[x] } ,F1()) = "\/" ( { ("\/" ( { F5(x9,y9) where x9 is Element of F2() : P1[x9] } ,F1())) where y9 is Element of F3() : P2[y9] } ,F1()) by A5; ::_thesis: verum end; Lm4: for x being Element of (RealPoset [.0,1.]) holds x is Real proof let x be Element of (RealPoset [.0,1.]); ::_thesis: x is Real ( x in the carrier of (RealPoset [.0,1.]) & the carrier of (RealPoset [.0,1.]) = [.0,1.] ) by Def3; hence x is Real ; ::_thesis: verum end; Lm5: for X, Y, Z being non empty set for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) proof let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let x be Element of X; ::_thesis: for z being Element of Z holds ( rng (min (R,S,x,z)) = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) let z be Element of Z; ::_thesis: ( rng (min (R,S,x,z)) = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} ) set L = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; A1: ( Y = dom (min (R,S,x,z)) & min (R,S,x,z) is PartFunc of (dom (min (R,S,x,z))),(rng (min (R,S,x,z))) ) by FUNCT_2:def_1, RELSET_1:4; for c being set holds ( c in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) ) proof let c be set ; ::_thesis: ( c in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) ) hereby ::_thesis: ( c in rng (min (R,S,x,z)) implies c in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ) assume c in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; ::_thesis: c in rng (min (R,S,x,z)) then consider y being Element of Y such that A2: c = (R . (x,y)) "/\" (S . (y,z)) ; c = (min (R,S,x,z)) . y by A2, FUZZY_4:def_2; hence c in rng (min (R,S,x,z)) by A1, PARTFUN1:4; ::_thesis: verum end; assume c in rng (min (R,S,x,z)) ; ::_thesis: c in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } then consider y being Element of Y such that y in dom (min (R,S,x,z)) and A3: c = (min (R,S,x,z)) . y by PARTFUN1:3; c = (R . (x,y)) "/\" (S . (y,z)) by A3, FUZZY_4:def_2; hence c in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; ::_thesis: verum end; hence rng (min (R,S,x,z)) = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } by TARSKI:1; ::_thesis: rng (min (R,S,x,z)) <> {} ex d being set st d in rng (min (R,S,x,z)) proof set y = the Element of Y; take (min (R,S,x,z)) . the Element of Y ; ::_thesis: (min (R,S,x,z)) . the Element of Y in rng (min (R,S,x,z)) thus (min (R,S,x,z)) . the Element of Y in rng (min (R,S,x,z)) by A1, PARTFUN1:4; ::_thesis: verum end; hence rng (min (R,S,x,z)) <> {} ; ::_thesis: verum end; theorem Th22: :: LFUZZY_0:22 for X, Y, Z being non empty set for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) proof let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let x be Element of X; ::_thesis: for z being Element of Z holds (R (#) S) . (x,z) = "\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let z be Element of Z; ::_thesis: (R (#) S) . (x,z) = "\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) set L = { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; [x,z] in [:X,Z:] ; then A1: (R (#) S) . (x,z) = upper_bound (rng (min (R,S,x,z))) by FUZZY_4:def_3; A2: for b being Element of (RealPoset [.0,1.]) st b is_>=_than { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } holds (R (#) S) . (x,z) <<= b proof let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b is_>=_than { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } implies (R (#) S) . (x,z) <<= b ) assume A3: b is_>=_than { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; ::_thesis: (R (#) S) . (x,z) <<= b A4: rng (min (R,S,x,z)) c= [.0,1.] by RELAT_1:def_19; A5: { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } = rng (min (R,S,x,z)) by Lm5; A6: for r being real number st r in rng (min (R,S,x,z)) holds r <= b proof let r be real number ; ::_thesis: ( r in rng (min (R,S,x,z)) implies r <= b ) assume A7: r in rng (min (R,S,x,z)) ; ::_thesis: r <= b then reconsider r = r as Element of (RealPoset [.0,1.]) by A4, Def3; r <<= b by A3, A5, A7, LATTICE3:def_9; hence r <= b by Th3; ::_thesis: verum end; rng (min (R,S,x,z)) <> {} by Lm5; then upper_bound (rng (min (R,S,x,z))) <= b by A6, SEQ_4:144; hence (R (#) S) . (x,z) <<= b by A1, Th3; ::_thesis: verum end; for b being Element of (RealPoset [.0,1.]) st b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } holds (R (#) S) . [x,z] >>= b proof let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } implies (R (#) S) . [x,z] >>= b ) assume b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; ::_thesis: (R (#) S) . [x,z] >>= b then consider y being Element of Y such that A8: b = (R . (x,y)) "/\" (S . (y,z)) and verum ; reconsider b = b as Real by Lm4; ( dom (min (R,S,x,z)) = Y & b = (min (R,S,x,z)) . y ) by A8, FUNCT_2:def_1, FUZZY_4:def_2; then b <= upper_bound (rng (min (R,S,x,z))) by FUZZY_4:1; hence (R (#) S) . [x,z] >>= b by A1, Th3; ::_thesis: verum end; then (R (#) S) . [x,z] is_>=_than { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } by LATTICE3:def_9; hence (R (#) S) . (x,z) = "\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) by A2, YELLOW_0:32; ::_thesis: verum end; Lm6: for X, Y, Z being non empty set for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.])) proof let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X for z being Element of Z for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let x be Element of X; ::_thesis: for z being Element of Z for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let z be Element of Z; ::_thesis: for a being Element of (RealPoset [.0,1.]) holds ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let a be Element of (RealPoset [.0,1.]); ::_thesis: ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.])) A1: { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } c= the carrier of (RealPoset [.0,1.]) proof let d be set ; :: according to TARSKI:def_3 ::_thesis: ( not d in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } or d in the carrier of (RealPoset [.0,1.]) ) assume d in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; ::_thesis: d in the carrier of (RealPoset [.0,1.]) then ex t being Element of Y st d = (R . (x,t)) "/\" (S . (t,z)) ; hence d in the carrier of (RealPoset [.0,1.]) ; ::_thesis: verum end; set A = { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } ; set B = { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ; A2: for c being set holds ( c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } iff c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ) proof let c be set ; ::_thesis: ( c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } iff c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ) hereby ::_thesis: ( c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } implies c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } ) assume c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } ; ::_thesis: c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } then consider b being Element of (RealPoset [.0,1.]) such that A3: c = b "/\" a and A4: b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ; ex y being Element of Y st b = (R . (x,y)) "/\" (S . (y,z)) by A4; hence c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } by A3; ::_thesis: verum end; assume c in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ; ::_thesis: c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } then consider y being Element of Y such that A5: c = ((R . (x,y)) "/\" (S . (y,z))) "/\" a ; (R . (x,y)) "/\" (S . (y,z)) in { ((R . (x,y1)) "/\" (S . (y1,z))) where y1 is Element of Y : verum } ; hence c in { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } by A5; ::_thesis: verum end; ((R (#) S) . (x,z)) "/\" a = ("\/" ( { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) "/\" a by Th22 .= "\/" ( { (b "/\" a) where b is Element of (RealPoset [.0,1.]) : b in { ((R . (x,y)) "/\" (S . (y,z))) where y is Element of Y : verum } } ,(RealPoset [.0,1.])) by A1, Th15 ; hence ((R (#) S) . (x,z)) "/\" a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ,(RealPoset [.0,1.])) by A2, TARSKI:1; ::_thesis: verum end; Lm7: for X, Y, Z being non empty set for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) proof let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z for x being Element of X for z being Element of Z for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X for z being Element of Z for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let x be Element of X; ::_thesis: for z being Element of Z for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let z be Element of Z; ::_thesis: for a being Element of (RealPoset [.0,1.]) holds a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) let a be Element of (RealPoset [.0,1.]); ::_thesis: a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) set A = { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ; set B = { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ; for b being set holds ( b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } iff b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ) proof let b be set ; ::_thesis: ( b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } iff b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ) hereby ::_thesis: ( b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } implies b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ) assume b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ; ::_thesis: b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } then consider y being Element of Y such that A1: b = (a "/\" (R . (x,y))) "/\" (S . (y,z)) ; b = ((R . (x,y)) "/\" (S . (y,z))) "/\" a by A1, LATTICE3:16; hence b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ; ::_thesis: verum end; assume b in { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } ; ::_thesis: b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } then consider y being Element of Y such that A2: b = ((R . (x,y)) "/\" (S . (y,z))) "/\" a ; b = (a "/\" (R . (x,y))) "/\" (S . (y,z)) by A2, LATTICE3:16; hence b in { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ; ::_thesis: verum end; then { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } = { (((R . (x,y)) "/\" (S . (y,z))) "/\" a) where y is Element of Y : verum } by TARSKI:1; hence a "/\" ((R (#) S) . (x,z)) = "\/" ( { ((a "/\" (R . (x,y))) "/\" (S . (y,z))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) by Lm6; ::_thesis: verum end; theorem :: LFUZZY_0:23 for X, Y, Z, W being non empty set for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T) proof let X, Y, Z, W be non empty set ; ::_thesis: for R being RMembership_Func of X,Y for S being RMembership_Func of Y,Z for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T) let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T) let S be RMembership_Func of Y,Z; ::_thesis: for T being RMembership_Func of Z,W holds (R (#) S) (#) T = R (#) (S (#) T) let T be RMembership_Func of Z,W; ::_thesis: (R (#) S) (#) T = R (#) (S (#) T) A1: for x, w being set st x in X & w in W holds ((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w) proof let x, w be set ; ::_thesis: ( x in X & w in W implies ((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w) ) assume that A2: x in X and A3: w in W ; ::_thesis: ((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w) reconsider w = w as Element of W by A3; reconsider x = x as Element of X by A2; set A = { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } ; set B = { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } ; set C = { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } ; set D = { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } ; defpred S1[ set ] means verum; deffunc H1( Element of Y, Element of Z) -> Element of the carrier of (RealPoset [.0,1.]) = ((R . (x,\$1)) "/\" (S . (\$1,\$2))) "/\" (T . (\$2,w)); A4: for a being set holds ( a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } iff a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } ) proof let a be set ; ::_thesis: ( a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } iff a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } ) hereby ::_thesis: ( a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } implies a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } ) assume a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } ; ::_thesis: a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } then consider z being Element of Z such that A5: a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) ; a = ((R (#) S) . (x,z)) "/\" (T . (z,w)) by A5, Lm6; hence a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } ; ::_thesis: verum end; assume a in { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } ; ::_thesis: a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } then consider z being Element of Z such that A6: a = ((R (#) S) . (x,z)) "/\" (T . (z,w)) ; a = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) by A6, Lm6; hence a in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.]))) where z is Element of Z : verum } ; ::_thesis: verum end; A7: for y being Element of Y for z being Element of Z st S1[y] & S1[z] holds H1(y,z) = H1(y,z) ; A8: "\/" ( { ("\/" ( { H1(y,z) where z is Element of Z : S1[z] } ,(RealPoset [.0,1.]))) where y is Element of Y : S1[y] } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { H1(y1,z1) where y1 is Element of Y : S1[y1] } ,(RealPoset [.0,1.]))) where z1 is Element of Z : S1[z1] } ,(RealPoset [.0,1.])) from LFUZZY_0:sch_5(A7); for c being set holds ( c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } iff c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } ) proof let c be set ; ::_thesis: ( c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } iff c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } ) hereby ::_thesis: ( c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } implies c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } ) assume c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } ; ::_thesis: c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } then consider y being Element of Y such that A9: c = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.])) ; c = (R . (x,y)) "/\" ((S (#) T) . (y,w)) by A9, Lm7; hence c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } ; ::_thesis: verum end; assume c in { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } ; ::_thesis: c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } then consider y being Element of Y such that A10: c = (R . (x,y)) "/\" ((S (#) T) . (y,w)) ; c = "\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.])) by A10, Lm7; hence c in { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } ; ::_thesis: verum end; then A11: { ("\/" ( { (((R . (x,y)) "/\" (S . (y,z))) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.]))) where y is Element of Y : verum } = { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } by TARSKI:1; ( ((R (#) S) (#) T) . (x,w) = "\/" ( { (((R (#) S) . (x,z)) "/\" (T . (z,w))) where z is Element of Z : verum } ,(RealPoset [.0,1.])) & (R (#) (S (#) T)) . (x,w) = "\/" ( { ((R . (x,y)) "/\" ((S (#) T) . (y,w))) where y is Element of Y : verum } ,(RealPoset [.0,1.])) ) by Th22; hence ((R (#) S) (#) T) . (x,w) = (R (#) (S (#) T)) . (x,w) by A4, A11, A8, TARSKI:1; ::_thesis: verum end; ( dom ((R (#) S) (#) T) = [:X,W:] & dom (R (#) (S (#) T)) = [:X,W:] ) by FUNCT_2:def_1; hence (R (#) S) (#) T = R (#) (S (#) T) by A1, FUNCT_3:6; ::_thesis: verum end;