:: YELLOW_7 semantic presentation begin notation let L be RelStr ; synonym L opp for L ~ ; end; theorem Th1: :: YELLOW_7:1 for L being RelStr for x, y being Element of (L opp) holds ( x <= y iff ~ x >= ~ y ) proof let L be RelStr ; ::_thesis: for x, y being Element of (L opp) holds ( x <= y iff ~ x >= ~ y ) let x, y be Element of (L opp); ::_thesis: ( x <= y iff ~ x >= ~ y ) ( (~ x) ~ = ~ x & (~ y) ~ = ~ y ) ; hence ( x <= y iff ~ x >= ~ y ) by LATTICE3:9; ::_thesis: verum end; theorem Th2: :: YELLOW_7:2 for L being RelStr for x being Element of L for y being Element of (L opp) holds ( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) ) proof let L be RelStr ; ::_thesis: for x being Element of L for y being Element of (L opp) holds ( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) ) let x be Element of L; ::_thesis: for y being Element of (L opp) holds ( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) ) let y be Element of (L opp); ::_thesis: ( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) ) ~ (x ~) = x ~ ; hence ( ( x <= ~ y implies x ~ >= y ) & ( x ~ >= y implies x <= ~ y ) & ( x >= ~ y implies x ~ <= y ) & ( x ~ <= y implies x >= ~ y ) ) by Th1; ::_thesis: verum end; theorem :: YELLOW_7:3 for L being RelStr holds ( L is empty iff L opp is empty ) ; theorem Th4: :: YELLOW_7:4 for L being RelStr holds ( L is reflexive iff L opp is reflexive ) proof let L be RelStr ; ::_thesis: ( L is reflexive iff L opp is reflexive ) thus ( L is reflexive implies L opp is reflexive ) ::_thesis: ( L opp is reflexive implies L is reflexive ) proof assume L is reflexive ; ::_thesis: L opp is reflexive then A1: the InternalRel of L is_reflexive_in the carrier of L by ORDERS_2:def_2; let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of (L opp) or [x,x] in the InternalRel of (L opp) ) assume x in the carrier of (L opp) ; ::_thesis: [x,x] in the InternalRel of (L opp) then [x,x] in the InternalRel of L by A1, RELAT_2:def_1; hence [x,x] in the InternalRel of (L opp) by RELAT_1:def_7; ::_thesis: verum end; assume L opp is reflexive ; ::_thesis: L is reflexive then A2: the InternalRel of (L opp) is_reflexive_in the carrier of (L opp) by ORDERS_2:def_2; let x be set ; :: according to RELAT_2:def_1,ORDERS_2:def_2 ::_thesis: ( not x in the carrier of L or [x,x] in the InternalRel of L ) assume x in the carrier of L ; ::_thesis: [x,x] in the InternalRel of L then [x,x] in the InternalRel of (L opp) by A2, RELAT_2:def_1; hence [x,x] in the InternalRel of L by RELAT_1:def_7; ::_thesis: verum end; theorem Th5: :: YELLOW_7:5 for L being RelStr holds ( L is antisymmetric iff L opp is antisymmetric ) proof let L be RelStr ; ::_thesis: ( L is antisymmetric iff L opp is antisymmetric ) thus ( L is antisymmetric implies L opp is antisymmetric ) ::_thesis: ( L opp is antisymmetric implies L is antisymmetric ) proof assume A1: L is antisymmetric ; ::_thesis: L opp is antisymmetric let x, y be Element of (L opp); :: 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 Th1; hence x = y by A1, YELLOW_0:def_3; ::_thesis: verum end; assume A2: L opp is antisymmetric ; ::_thesis: L is antisymmetric let x, y be Element of L; :: 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 LATTICE3:9; hence x = y by A2, YELLOW_0:def_3; ::_thesis: verum end; theorem Th6: :: YELLOW_7:6 for L being RelStr holds ( L is transitive iff L opp is transitive ) proof let L be RelStr ; ::_thesis: ( L is transitive iff L opp is transitive ) thus ( L is transitive implies L opp is transitive ) ::_thesis: ( L opp is transitive implies L is transitive ) proof assume A1: L is transitive ; ::_thesis: L opp is transitive let x, y, z be Element of (L opp); :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume ( x <= y & z >= y ) ; ::_thesis: x <= z then ( ~ x >= ~ y & ~ z <= ~ y ) by Th1; then ~ x >= ~ z by A1, YELLOW_0:def_2; hence x <= z by Th1; ::_thesis: verum end; assume A2: L opp is transitive ; ::_thesis: L is transitive let x, y, z be Element of L; :: according to YELLOW_0:def_2 ::_thesis: ( not x <= y or not y <= z or x <= z ) assume ( x <= y & z >= y ) ; ::_thesis: x <= z then ( x ~ >= y ~ & z ~ <= y ~ ) by LATTICE3:9; then x ~ >= z ~ by A2, YELLOW_0:def_2; hence x <= z by LATTICE3:9; ::_thesis: verum end; theorem Th7: :: YELLOW_7:7 for L being non empty RelStr holds ( L is connected iff L opp is connected ) proof let L be non empty RelStr ; ::_thesis: ( L is connected iff L opp is connected ) thus ( L is connected implies L opp is connected ) ::_thesis: ( L opp is connected implies L is connected ) proof assume A1: for x, y being Element of L holds ( x <= y or x >= y ) ; :: according to WAYBEL_0:def_29 ::_thesis: L opp is connected let x, y be Element of (L opp); :: according to WAYBEL_0:def_29 ::_thesis: ( x <= y or y <= x ) ( ~ x <= ~ y or ~ x >= ~ y ) by A1; hence ( x <= y or y <= x ) by Th1; ::_thesis: verum end; assume A2: for x, y being Element of (L opp) holds ( x <= y or x >= y ) ; :: according to WAYBEL_0:def_29 ::_thesis: L is connected let x, y be Element of L; :: according to WAYBEL_0:def_29 ::_thesis: ( x <= y or y <= x ) ( x ~ <= y ~ or x ~ >= y ~ ) by A2; hence ( x <= y or y <= x ) by LATTICE3:9; ::_thesis: verum end; registration let L be reflexive RelStr ; clusterL opp -> reflexive ; coherence L opp is reflexive by Th4; end; registration let L be transitive RelStr ; clusterL opp -> transitive ; coherence L opp is transitive by Th6; end; registration let L be antisymmetric RelStr ; clusterL opp -> antisymmetric ; coherence L opp is antisymmetric by Th5; end; registration let L be non empty connected RelStr ; clusterL opp -> connected ; coherence L opp is connected by Th7; end; theorem Th8: :: YELLOW_7:8 for L being RelStr for x being Element of L for X being set holds ( ( x is_<=_than X implies x ~ is_>=_than X ) & ( x ~ is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies x ~ is_<=_than X ) & ( x ~ is_<=_than X implies x is_>=_than X ) ) proof let L be RelStr ; ::_thesis: for x being Element of L for X being set holds ( ( x is_<=_than X implies x ~ is_>=_than X ) & ( x ~ is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies x ~ is_<=_than X ) & ( x ~ is_<=_than X implies x is_>=_than X ) ) let x be Element of L; ::_thesis: for X being set holds ( ( x is_<=_than X implies x ~ is_>=_than X ) & ( x ~ is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies x ~ is_<=_than X ) & ( x ~ is_<=_than X implies x is_>=_than X ) ) let X be set ; ::_thesis: ( ( x is_<=_than X implies x ~ is_>=_than X ) & ( x ~ is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies x ~ is_<=_than X ) & ( x ~ is_<=_than X implies x is_>=_than X ) ) A1: now__::_thesis:_for_L_being_RelStr_ for_x_being_Element_of_L for_X_being_set_st_x_is_<=_than_X_holds_ x_~_is_>=_than_X let L be RelStr ; ::_thesis: for x being Element of L for X being set st x is_<=_than X holds x ~ is_>=_than X let x be Element of L; ::_thesis: for X being set st x is_<=_than X holds x ~ is_>=_than X let X be set ; ::_thesis: ( x is_<=_than X implies x ~ is_>=_than X ) assume A2: x is_<=_than X ; ::_thesis: x ~ is_>=_than X thus x ~ is_>=_than X ::_thesis: verum proof let a be Element of (L opp); :: according to LATTICE3:def_9 ::_thesis: ( not a in X or a <= x ~ ) assume a in X ; ::_thesis: a <= x ~ then ( (~ a) ~ = ~ a & x <= ~ a ) by A2, LATTICE3:def_8; hence a <= x ~ by LATTICE3:9; ::_thesis: verum end; end; A3: now__::_thesis:_for_L_being_RelStr_ for_x_being_Element_of_L for_X_being_set_st_x_is_>=_than_X_holds_ x_~_is_<=_than_X let L be RelStr ; ::_thesis: for x being Element of L for X being set st x is_>=_than X holds x ~ is_<=_than X let x be Element of L; ::_thesis: for X being set st x is_>=_than X holds x ~ is_<=_than X let X be set ; ::_thesis: ( x is_>=_than X implies x ~ is_<=_than X ) assume A4: x is_>=_than X ; ::_thesis: x ~ is_<=_than X thus x ~ is_<=_than X ::_thesis: verum proof let a be Element of (L opp); :: according to LATTICE3:def_8 ::_thesis: ( not a in X or x ~ <= a ) assume a in X ; ::_thesis: x ~ <= a then ( (~ a) ~ = ~ a & x >= ~ a ) by A4, LATTICE3:def_9; hence x ~ <= a by LATTICE3:9; ::_thesis: verum end; end; ( (x ~) ~ is_<=_than X implies x is_<=_than X ) by YELLOW_0:2; hence ( x is_<=_than X iff x ~ is_>=_than X ) by A1, A3; ::_thesis: ( x is_>=_than X iff x ~ is_<=_than X ) ( (x ~) ~ is_>=_than X implies x is_>=_than X ) by YELLOW_0:2; hence ( x is_>=_than X iff x ~ is_<=_than X ) by A1, A3; ::_thesis: verum end; theorem Th9: :: YELLOW_7:9 for L being RelStr for x being Element of (L opp) for X being set holds ( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) ) proof let L be RelStr ; ::_thesis: for x being Element of (L opp) for X being set holds ( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) ) let x be Element of (L opp); ::_thesis: for X being set holds ( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) ) let X be set ; ::_thesis: ( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) ) (~ x) ~ = ~ x ; hence ( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) ) by Th8; ::_thesis: verum end; theorem Th10: :: YELLOW_7:10 for L being RelStr for X being set holds ( ex_sup_of X,L iff ex_inf_of X,L opp ) proof let L be RelStr ; ::_thesis: for X being set holds ( ex_sup_of X,L iff ex_inf_of X,L opp ) let X be set ; ::_thesis: ( ex_sup_of X,L iff ex_inf_of X,L opp ) hereby ::_thesis: ( ex_inf_of X,L opp implies ex_sup_of X,L ) assume ex_sup_of X,L ; ::_thesis: ex_inf_of X,L opp then consider a being Element of L such that A1: X is_<=_than a and A2: for b being Element of L st X is_<=_than b holds b >= a and A3: for c being Element of L st X is_<=_than c & ( for b being Element of L st X is_<=_than b holds b >= c ) holds c = a by YELLOW_0:def_7; thus ex_inf_of X,L opp ::_thesis: verum proof take a ~ ; :: according to YELLOW_0:def_8 ::_thesis: ( a ~ is_<=_than X & ( for b1 being Element of the carrier of (L opp) holds ( not b1 is_<=_than X or b1 <= a ~ ) ) & ( for b1 being Element of the carrier of (L opp) holds ( not b1 is_<=_than X or ex b2 being Element of the carrier of (L opp) st ( b2 is_<=_than X & not b2 <= b1 ) or b1 = a ~ ) ) ) thus X is_>=_than a ~ by A1, Th8; ::_thesis: ( ( for b1 being Element of the carrier of (L opp) holds ( not b1 is_<=_than X or b1 <= a ~ ) ) & ( for b1 being Element of the carrier of (L opp) holds ( not b1 is_<=_than X or ex b2 being Element of the carrier of (L opp) st ( b2 is_<=_than X & not b2 <= b1 ) or b1 = a ~ ) ) ) hereby ::_thesis: for b1 being Element of the carrier of (L opp) holds ( not b1 is_<=_than X or ex b2 being Element of the carrier of (L opp) st ( b2 is_<=_than X & not b2 <= b1 ) or b1 = a ~ ) let b be Element of (L opp); ::_thesis: ( X is_>=_than b implies b <= a ~ ) assume X is_>=_than b ; ::_thesis: b <= a ~ then X is_<=_than ~ b by Th9; then ~ b >= a by A2; hence b <= a ~ by Th2; ::_thesis: verum end; let c be Element of (L opp); ::_thesis: ( not c is_<=_than X or ex b1 being Element of the carrier of (L opp) st ( b1 is_<=_than X & not b1 <= c ) or c = a ~ ) assume X is_>=_than c ; ::_thesis: ( ex b1 being Element of the carrier of (L opp) st ( b1 is_<=_than X & not b1 <= c ) or c = a ~ ) then A4: X is_<=_than ~ c by Th9; assume A5: for b being Element of (L opp) st X is_>=_than b holds b <= c ; ::_thesis: c = a ~ now__::_thesis:_for_b_being_Element_of_L_st_X_is_<=_than_b_holds_ b_>=_~_c let b be Element of L; ::_thesis: ( X is_<=_than b implies b >= ~ c ) assume X is_<=_than b ; ::_thesis: b >= ~ c then X is_>=_than b ~ by Th8; then b ~ <= c by A5; hence b >= ~ c by Th2; ::_thesis: verum end; hence c = a ~ by A3, A4; ::_thesis: verum end; end; assume ex_inf_of X,L opp ; ::_thesis: ex_sup_of X,L then consider a being Element of (L opp) such that A6: X is_>=_than a and A7: for b being Element of (L opp) st X is_>=_than b holds b <= a and A8: for c being Element of (L opp) st X is_>=_than c & ( for b being Element of (L opp) st X is_>=_than b holds b <= c ) holds c = a by YELLOW_0:def_8; take ~ a ; :: according to YELLOW_0:def_7 ::_thesis: ( X is_<=_than ~ a & ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or ~ a <= b1 ) ) & ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or ex b2 being Element of the carrier of L st ( X is_<=_than b2 & not b1 <= b2 ) or b1 = ~ a ) ) ) thus X is_<=_than ~ a by A6, Th9; ::_thesis: ( ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or ~ a <= b1 ) ) & ( for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or ex b2 being Element of the carrier of L st ( X is_<=_than b2 & not b1 <= b2 ) or b1 = ~ a ) ) ) hereby ::_thesis: for b1 being Element of the carrier of L holds ( not X is_<=_than b1 or ex b2 being Element of the carrier of L st ( X is_<=_than b2 & not b1 <= b2 ) or b1 = ~ a ) let b be Element of L; ::_thesis: ( X is_<=_than b implies b >= ~ a ) assume X is_<=_than b ; ::_thesis: b >= ~ a then X is_>=_than b ~ by Th8; then b ~ <= a by A7; hence b >= ~ a by Th2; ::_thesis: verum end; let c be Element of L; ::_thesis: ( not X is_<=_than c or ex b1 being Element of the carrier of L st ( X is_<=_than b1 & not c <= b1 ) or c = ~ a ) assume X is_<=_than c ; ::_thesis: ( ex b1 being Element of the carrier of L st ( X is_<=_than b1 & not c <= b1 ) or c = ~ a ) then A9: X is_>=_than c ~ by Th8; assume A10: for b being Element of L st X is_<=_than b holds b >= c ; ::_thesis: c = ~ a now__::_thesis:_for_b_being_Element_of_(L_opp)_st_X_is_>=_than_b_holds_ b_<=_c_~ let b be Element of (L opp); ::_thesis: ( X is_>=_than b implies b <= c ~ ) assume X is_>=_than b ; ::_thesis: b <= c ~ then X is_<=_than ~ b by Th9; then ~ b >= c by A10; hence b <= c ~ by Th2; ::_thesis: verum end; hence c = ~ a by A8, A9; ::_thesis: verum end; theorem Th11: :: YELLOW_7:11 for L being RelStr for X being set holds ( ex_sup_of X,L opp iff ex_inf_of X,L ) proof let L be RelStr ; ::_thesis: for X being set holds ( ex_sup_of X,L opp iff ex_inf_of X,L ) let X be set ; ::_thesis: ( ex_sup_of X,L opp iff ex_inf_of X,L ) ( ex_inf_of X,L iff ex_inf_of X,(L opp) ~ ) by YELLOW_0:14; hence ( ex_sup_of X,L opp iff ex_inf_of X,L ) by Th10; ::_thesis: verum end; theorem Th12: :: YELLOW_7:12 for L being non empty RelStr for X being set st ( ex_sup_of X,L or ex_inf_of X,L opp ) holds "\/" (X,L) = "/\" (X,(L opp)) proof let L be non empty RelStr ; ::_thesis: for X being set st ( ex_sup_of X,L or ex_inf_of X,L opp ) holds "\/" (X,L) = "/\" (X,(L opp)) let X be set ; ::_thesis: ( ( ex_sup_of X,L or ex_inf_of X,L opp ) implies "\/" (X,L) = "/\" (X,(L opp)) ) assume A1: ( ex_sup_of X,L or ex_inf_of X,L opp ) ; ::_thesis: "\/" (X,L) = "/\" (X,(L opp)) then A2: ex_sup_of X,L by Th10; then "\/" (X,L) is_>=_than X by YELLOW_0:def_9; then A3: ("\/" (X,L)) ~ is_<=_than X by Th8; A4: now__::_thesis:_for_x_being_Element_of_(L_opp)_st_x_is_<=_than_X_holds_ x_<=_("\/"_(X,L))_~ let x be Element of (L opp); ::_thesis: ( x is_<=_than X implies x <= ("\/" (X,L)) ~ ) assume x is_<=_than X ; ::_thesis: x <= ("\/" (X,L)) ~ then ~ x is_>=_than X by Th9; then ~ x >= "\/" (X,L) by A2, YELLOW_0:def_9; hence x <= ("\/" (X,L)) ~ by Th2; ::_thesis: verum end; ex_inf_of X,L opp by A1, Th10; hence "\/" (X,L) = "/\" (X,(L opp)) by A3, A4, YELLOW_0:def_10; ::_thesis: verum end; theorem Th13: :: YELLOW_7:13 for L being non empty RelStr for X being set st ( ex_inf_of X,L or ex_sup_of X,L opp ) holds "/\" (X,L) = "\/" (X,(L opp)) proof let L be non empty RelStr ; ::_thesis: for X being set st ( ex_inf_of X,L or ex_sup_of X,L opp ) holds "/\" (X,L) = "\/" (X,(L opp)) let X be set ; ::_thesis: ( ( ex_inf_of X,L or ex_sup_of X,L opp ) implies "/\" (X,L) = "\/" (X,(L opp)) ) assume A1: ( ex_inf_of X,L or ex_sup_of X,L opp ) ; ::_thesis: "/\" (X,L) = "\/" (X,(L opp)) then A2: ex_inf_of X,L by Th11; then "/\" (X,L) is_<=_than X by YELLOW_0:def_10; then A3: ("/\" (X,L)) ~ is_>=_than X by Th8; A4: now__::_thesis:_for_x_being_Element_of_(L_opp)_st_x_is_>=_than_X_holds_ x_>=_("/\"_(X,L))_~ let x be Element of (L opp); ::_thesis: ( x is_>=_than X implies x >= ("/\" (X,L)) ~ ) assume x is_>=_than X ; ::_thesis: x >= ("/\" (X,L)) ~ then ~ x is_<=_than X by Th9; then ~ x <= "/\" (X,L) by A2, YELLOW_0:def_10; hence x >= ("/\" (X,L)) ~ by Th2; ::_thesis: verum end; ex_sup_of X,L opp by A1, Th11; hence "/\" (X,L) = "\/" (X,(L opp)) by A3, A4, YELLOW_0:def_9; ::_thesis: verum end; theorem Th14: :: YELLOW_7:14 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is with_infima holds L2 is with_infima proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is with_infima implies L2 is with_infima ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: for x, y being Element of L1 ex z being Element of L1 st ( z <= x & z <= y & ( for z9 being Element of L1 st z9 <= x & z9 <= y holds z9 <= z ) ) ; :: according to LATTICE3:def_11 ::_thesis: L2 is with_infima let a, b be Element of L2; :: according to LATTICE3:def_11 ::_thesis: ex b1 being Element of the carrier of L2 st ( b1 <= a & b1 <= b & ( for b2 being Element of the carrier of L2 holds ( not b2 <= a or not b2 <= b or b2 <= b1 ) ) ) reconsider x = a, y = b as Element of L1 by A1; consider z being Element of L1 such that A3: ( z <= x & z <= y ) and A4: for z9 being Element of L1 st z9 <= x & z9 <= y holds z9 <= z by A2; reconsider c = z as Element of L2 by A1; take c ; ::_thesis: ( c <= a & c <= b & ( for b1 being Element of the carrier of L2 holds ( not b1 <= a or not b1 <= b or b1 <= c ) ) ) thus ( c <= a & c <= b ) by A1, A3, YELLOW_0:1; ::_thesis: for b1 being Element of the carrier of L2 holds ( not b1 <= a or not b1 <= b or b1 <= c ) let d be Element of L2; ::_thesis: ( not d <= a or not d <= b or d <= c ) reconsider z9 = d as Element of L1 by A1; assume ( d <= a & d <= b ) ; ::_thesis: d <= c then ( z9 <= x & z9 <= y ) by A1, YELLOW_0:1; then z9 <= z by A4; hence d <= c by A1, YELLOW_0:1; ::_thesis: verum end; theorem :: YELLOW_7:15 for L1, L2 being RelStr st RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is with_suprema holds L2 is with_suprema proof let L1, L2 be RelStr ; ::_thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) & L1 is with_suprema implies L2 is with_suprema ) assume that A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) and A2: for x, y being Element of L1 ex z being Element of L1 st ( z >= x & z >= y & ( for z9 being Element of L1 st z9 >= x & z9 >= y holds z9 >= z ) ) ; :: according to LATTICE3:def_10 ::_thesis: L2 is with_suprema let a, b be Element of L2; :: according to LATTICE3:def_10 ::_thesis: ex b1 being Element of the carrier of L2 st ( a <= b1 & b <= b1 & ( for b2 being Element of the carrier of L2 holds ( not a <= b2 or not b <= b2 or b1 <= b2 ) ) ) reconsider x = a, y = b as Element of L1 by A1; consider z being Element of L1 such that A3: ( z >= x & z >= y ) and A4: for z9 being Element of L1 st z9 >= x & z9 >= y holds z9 >= z by A2; reconsider c = z as Element of L2 by A1; take c ; ::_thesis: ( a <= c & b <= c & ( for b1 being Element of the carrier of L2 holds ( not a <= b1 or not b <= b1 or c <= b1 ) ) ) thus ( c >= a & c >= b ) by A1, A3, YELLOW_0:1; ::_thesis: for b1 being Element of the carrier of L2 holds ( not a <= b1 or not b <= b1 or c <= b1 ) let d be Element of L2; ::_thesis: ( not a <= d or not b <= d or c <= d ) reconsider z9 = d as Element of L1 by A1; assume ( d >= a & d >= b ) ; ::_thesis: c <= d then ( z9 >= x & z9 >= y ) by A1, YELLOW_0:1; then z9 >= z by A4; hence c <= d by A1, YELLOW_0:1; ::_thesis: verum end; theorem Th16: :: YELLOW_7:16 for L being RelStr holds ( L is with_infima iff L opp is with_suprema ) proof let L be RelStr ; ::_thesis: ( L is with_infima iff L opp is with_suprema ) ( L is with_infima iff (L opp) ~ is with_infima ) by Th14; hence ( L is with_infima iff L opp is with_suprema ) by LATTICE3:10; ::_thesis: verum end; theorem Th17: :: YELLOW_7:17 for L being non empty RelStr holds ( L is complete iff L opp is complete ) proof let L be non empty RelStr ; ::_thesis: ( L is complete iff L opp is complete ) A1: now__::_thesis:_for_L_being_non_empty_RelStr_st_L_is_complete_holds_ L_opp_is_complete let L be non empty RelStr ; ::_thesis: ( L is complete implies L opp is complete ) assume A2: L is complete ; ::_thesis: L opp is complete thus L opp is complete ::_thesis: verum proof let X be set ; :: according to LATTICE3:def_12 ::_thesis: ex b1 being Element of the carrier of (L opp) st ( X is_<=_than b1 & ( for b2 being Element of the carrier of (L opp) holds ( not X is_<=_than b2 or b1 <= b2 ) ) ) set Y = { x where x is Element of L : x is_<=_than X } ; consider a being Element of L such that A3: { x where x is Element of L : x is_<=_than X } is_<=_than a and A4: for b being Element of L st { x where x is Element of L : x is_<=_than X } is_<=_than b holds a <= b by A2, LATTICE3:def_12; take x = a ~ ; ::_thesis: ( X is_<=_than x & ( for b1 being Element of the carrier of (L opp) holds ( not X is_<=_than b1 or x <= b1 ) ) ) thus X is_<=_than x ::_thesis: for b1 being Element of the carrier of (L opp) holds ( not X is_<=_than b1 or x <= b1 ) proof let y be Element of (L opp); :: according to LATTICE3:def_9 ::_thesis: ( not y in X or y <= x ) assume A5: y in X ; ::_thesis: y <= x { x where x is Element of L : x is_<=_than X } is_<=_than ~ y proof let b be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not b in { x where x is Element of L : x is_<=_than X } or b <= ~ y ) assume b in { x where x is Element of L : x is_<=_than X } ; ::_thesis: b <= ~ y then ex z being Element of L st ( b = z & z is_<=_than X ) ; hence b <= ~ y by A5, LATTICE3:def_8; ::_thesis: verum end; then a <= ~ y by A4; hence y <= x by Th2; ::_thesis: verum end; let y be Element of (L opp); ::_thesis: ( not X is_<=_than y or x <= y ) assume X is_<=_than y ; ::_thesis: x <= y then X is_>=_than ~ y by Th9; then ~ y in { x where x is Element of L : x is_<=_than X } ; then A6: a >= ~ y by A3, LATTICE3:def_9; ~ x = x ; hence x <= y by A6, Th1; ::_thesis: verum end; end; ( (L opp) ~ is complete implies L is complete ) by YELLOW_0:3; hence ( L is complete iff L opp is complete ) by A1; ::_thesis: verum end; registration let L be with_infima RelStr ; clusterL opp -> with_suprema ; coherence L opp is with_suprema by Th16; end; registration let L be with_suprema RelStr ; clusterL opp -> with_infima ; coherence L opp is with_infima by LATTICE3:10; end; registration let L be non empty complete RelStr ; clusterL opp -> complete ; coherence L opp is complete by Th17; end; theorem :: YELLOW_7:18 for L being non empty RelStr for X being Subset of L for Y being Subset of (L opp) st X = Y holds ( fininfs X = finsups Y & finsups X = fininfs Y ) proof let L be non empty RelStr ; ::_thesis: for X being Subset of L for Y being Subset of (L opp) st X = Y holds ( fininfs X = finsups Y & finsups X = fininfs Y ) let X be Subset of L; ::_thesis: for Y being Subset of (L opp) st X = Y holds ( fininfs X = finsups Y & finsups X = fininfs Y ) let Y be Subset of (L opp); ::_thesis: ( X = Y implies ( fininfs X = finsups Y & finsups X = fininfs Y ) ) assume A1: X = Y ; ::_thesis: ( fininfs X = finsups Y & finsups X = fininfs Y ) thus fininfs X c= finsups Y :: according to XBOOLE_0:def_10 ::_thesis: ( finsups Y c= fininfs X & finsups X = fininfs Y ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in fininfs X or x in finsups Y ) assume x in fininfs X ; ::_thesis: x in finsups Y then consider Z being finite Subset of X such that A2: ( x = "/\" (Z,L) & ex_inf_of Z,L ) ; ( x = "\/" (Z,(L opp)) & ex_sup_of Z,L opp ) by A2, Th11, Th13; hence x in finsups Y by A1; ::_thesis: verum end; thus finsups Y c= fininfs X ::_thesis: finsups X = fininfs Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in finsups Y or x in fininfs X ) assume x in finsups Y ; ::_thesis: x in fininfs X then consider Z being finite Subset of Y such that A3: ( x = "\/" (Z,(L opp)) & ex_sup_of Z,L opp ) ; ( x = "/\" (Z,L) & ex_inf_of Z,L ) by A3, Th11, Th13; hence x in fininfs X by A1; ::_thesis: verum end; thus finsups X c= fininfs Y :: according to XBOOLE_0:def_10 ::_thesis: fininfs Y c= finsups X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in finsups X or x in fininfs Y ) assume x in finsups X ; ::_thesis: x in fininfs Y then consider Z being finite Subset of X such that A4: ( x = "\/" (Z,L) & ex_sup_of Z,L ) ; ( x = "/\" (Z,(L opp)) & ex_inf_of Z,L opp ) by A4, Th10, Th12; hence x in fininfs Y by A1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in fininfs Y or x in finsups X ) assume x in fininfs Y ; ::_thesis: x in finsups X then consider Z being finite Subset of Y such that A5: ( x = "/\" (Z,(L opp)) & ex_inf_of Z,L opp ) ; ( x = "\/" (Z,L) & ex_sup_of Z,L ) by A5, Th10, Th12; hence x in finsups X by A1; ::_thesis: verum end; theorem Th19: :: YELLOW_7:19 for L being RelStr for X being Subset of L for Y being Subset of (L opp) st X = Y holds ( downarrow X = uparrow Y & uparrow X = downarrow Y ) proof let L be RelStr ; ::_thesis: for X being Subset of L for Y being Subset of (L opp) st X = Y holds ( downarrow X = uparrow Y & uparrow X = downarrow Y ) let X be Subset of L; ::_thesis: for Y being Subset of (L opp) st X = Y holds ( downarrow X = uparrow Y & uparrow X = downarrow Y ) let Y be Subset of (L opp); ::_thesis: ( X = Y implies ( downarrow X = uparrow Y & uparrow X = downarrow Y ) ) assume A1: X = Y ; ::_thesis: ( downarrow X = uparrow Y & uparrow X = downarrow Y ) thus downarrow X c= uparrow Y :: according to XBOOLE_0:def_10 ::_thesis: ( uparrow Y c= downarrow X & uparrow X = downarrow Y ) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow X or x in uparrow Y ) assume A2: x in downarrow X ; ::_thesis: x in uparrow Y then reconsider x = x as Element of L ; consider y being Element of L such that A3: y >= x and A4: y in X by A2, WAYBEL_0:def_15; y ~ <= x ~ by A3, LATTICE3:9; hence x in uparrow Y by A1, A4, WAYBEL_0:def_16; ::_thesis: verum end; thus uparrow Y c= downarrow X ::_thesis: uparrow X = downarrow Y proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow Y or x in downarrow X ) assume A5: x in uparrow Y ; ::_thesis: x in downarrow X then reconsider x = x as Element of (L opp) ; consider y being Element of (L opp) such that A6: y <= x and A7: y in Y by A5, WAYBEL_0:def_16; ~ y >= ~ x by A6, Th1; hence x in downarrow X by A1, A7, WAYBEL_0:def_15; ::_thesis: verum end; thus uparrow X c= downarrow Y :: according to XBOOLE_0:def_10 ::_thesis: downarrow Y c= uparrow X proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in uparrow X or x in downarrow Y ) assume A8: x in uparrow X ; ::_thesis: x in downarrow Y then reconsider x = x as Element of L ; consider y being Element of L such that A9: y <= x and A10: y in X by A8, WAYBEL_0:def_16; y ~ >= x ~ by A9, LATTICE3:9; hence x in downarrow Y by A1, A10, WAYBEL_0:def_15; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in downarrow Y or x in uparrow X ) assume A11: x in downarrow Y ; ::_thesis: x in uparrow X then reconsider x = x as Element of (L opp) ; consider y being Element of (L opp) such that A12: y >= x and A13: y in Y by A11, WAYBEL_0:def_15; ~ y <= ~ x by A12, Th1; hence x in uparrow X by A1, A13, WAYBEL_0:def_16; ::_thesis: verum end; theorem :: YELLOW_7:20 for L being non empty RelStr for x being Element of L for y being Element of (L opp) st x = y holds ( downarrow x = uparrow y & uparrow x = downarrow y ) by Th19; theorem Th21: :: YELLOW_7:21 for L being with_infima Poset for x, y being Element of L holds x "/\" y = (x ~) "\/" (y ~) proof let L be with_infima Poset; ::_thesis: for x, y being Element of L holds x "/\" y = (x ~) "\/" (y ~) let x, y be Element of L; ::_thesis: x "/\" y = (x ~) "\/" (y ~) x "/\" y <= y by YELLOW_0:23; then A1: (x "/\" y) ~ >= y ~ by LATTICE3:9; A2: ( ~ (x ~) = x ~ & ~ (y ~) = y ~ ) ; A3: now__::_thesis:_for_d_being_Element_of_(L_opp)_st_d_>=_x_~_&_d_>=_y_~_holds_ (x_"/\"_y)_~_<=_d let d be Element of (L opp); ::_thesis: ( d >= x ~ & d >= y ~ implies (x "/\" y) ~ <= d ) assume ( d >= x ~ & d >= y ~ ) ; ::_thesis: (x "/\" y) ~ <= d then ( ~ d <= x & ~ d <= y ) by A2, Th1; then A4: ~ d <= x "/\" y by YELLOW_0:23; (~ d) ~ = ~ d ; hence (x "/\" y) ~ <= d by A4, LATTICE3:9; ::_thesis: verum end; x "/\" y <= x by YELLOW_0:23; then (x "/\" y) ~ >= x ~ by LATTICE3:9; hence x "/\" y = (x ~) "\/" (y ~) by A1, A3, YELLOW_0:22; ::_thesis: verum end; theorem Th22: :: YELLOW_7:22 for L being with_infima Poset for x, y being Element of (L opp) holds (~ x) "/\" (~ y) = x "\/" y proof let L be with_infima Poset; ::_thesis: for x, y being Element of (L opp) holds (~ x) "/\" (~ y) = x "\/" y let x, y be Element of (L opp); ::_thesis: (~ x) "/\" (~ y) = x "\/" y ( (~ x) ~ = ~ x & (~ y) ~ = ~ y ) ; hence (~ x) "/\" (~ y) = x "\/" y by Th21; ::_thesis: verum end; theorem Th23: :: YELLOW_7:23 for L being with_suprema Poset for x, y being Element of L holds x "\/" y = (x ~) "/\" (y ~) proof let L be with_suprema Poset; ::_thesis: for x, y being Element of L holds x "\/" y = (x ~) "/\" (y ~) let x, y be Element of L; ::_thesis: x "\/" y = (x ~) "/\" (y ~) x "\/" y >= y by YELLOW_0:22; then A1: (x "\/" y) ~ <= y ~ by LATTICE3:9; A2: ( ~ (x ~) = x ~ & ~ (y ~) = y ~ ) ; A3: now__::_thesis:_for_d_being_Element_of_(L_opp)_st_d_<=_x_~_&_d_<=_y_~_holds_ (x_"\/"_y)_~_>=_d let d be Element of (L opp); ::_thesis: ( d <= x ~ & d <= y ~ implies (x "\/" y) ~ >= d ) assume ( d <= x ~ & d <= y ~ ) ; ::_thesis: (x "\/" y) ~ >= d then ( ~ d >= x & ~ d >= y ) by A2, Th1; then A4: ~ d >= x "\/" y by YELLOW_0:22; (~ d) ~ = ~ d ; hence (x "\/" y) ~ >= d by A4, LATTICE3:9; ::_thesis: verum end; x "\/" y >= x by YELLOW_0:22; then (x "\/" y) ~ <= x ~ by LATTICE3:9; hence x "\/" y = (x ~) "/\" (y ~) by A1, A3, YELLOW_0:23; ::_thesis: verum end; theorem Th24: :: YELLOW_7:24 for L being with_suprema Poset for x, y being Element of (L opp) holds (~ x) "\/" (~ y) = x "/\" y proof let L be with_suprema Poset; ::_thesis: for x, y being Element of (L opp) holds (~ x) "\/" (~ y) = x "/\" y let x, y be Element of (L opp); ::_thesis: (~ x) "\/" (~ y) = x "/\" y ( (~ x) ~ = ~ x & (~ y) ~ = ~ y ) ; hence (~ x) "\/" (~ y) = x "/\" y by Th23; ::_thesis: verum end; theorem Th25: :: YELLOW_7:25 for L being LATTICE holds ( L is distributive iff L opp is distributive ) proof let L be LATTICE; ::_thesis: ( L is distributive iff L opp is distributive ) hereby ::_thesis: ( L opp is distributive implies L is distributive ) assume A1: L is distributive ; ::_thesis: L opp is distributive thus L opp is distributive ::_thesis: verum proof let x, y, z be Element of (L opp); :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) thus x "/\" (y "\/" z) = (~ x) "\/" (~ (y "\/" z)) by Th24 .= (~ x) "\/" ((~ y) "/\" (~ z)) by Th22 .= ((~ x) "\/" (~ y)) "/\" ((~ x) "\/" (~ z)) by A1, WAYBEL_1:5 .= (~ (x "/\" y)) "/\" ((~ x) "\/" (~ z)) by Th24 .= (~ (x "/\" y)) "/\" (~ (x "/\" z)) by Th24 .= (x "/\" y) "\/" (x "/\" z) by Th22 ; ::_thesis: verum end; end; assume A2: L opp is distributive ; ::_thesis: L is distributive let x, y, z be Element of L; :: according to WAYBEL_1:def_3 ::_thesis: x "/\" (y "\/" z) = (x "/\" y) "\/" (x "/\" z) thus x "/\" (y "\/" z) = (x ~) "\/" ((y "\/" z) ~) by Th21 .= (x ~) "\/" ((y ~) "/\" (z ~)) by Th23 .= ((x ~) "\/" (y ~)) "/\" ((x ~) "\/" (z ~)) by A2, WAYBEL_1:5 .= ((x "/\" y) ~) "/\" ((x ~) "\/" (z ~)) by Th21 .= ((x "/\" y) ~) "/\" ((x "/\" z) ~) by Th21 .= (x "/\" y) "\/" (x "/\" z) by Th23 ; ::_thesis: verum end; registration let L be distributive LATTICE; clusterL opp -> distributive ; coherence L opp is distributive by Th25; end; theorem Th26: :: YELLOW_7:26 for L being RelStr for x being set holds ( x is directed Subset of L iff x is filtered Subset of (L opp) ) proof let L be RelStr ; ::_thesis: for x being set holds ( x is directed Subset of L iff x is filtered Subset of (L opp) ) let x be set ; ::_thesis: ( x is directed Subset of L iff x is filtered Subset of (L opp) ) hereby ::_thesis: ( x is filtered Subset of (L opp) implies x is directed Subset of L ) assume x is directed Subset of L ; ::_thesis: x is filtered Subset of (L opp) then reconsider X = x as directed Subset of L ; reconsider Y = X as Subset of (L opp) ; Y is filtered proof let x, y be Element of (L opp); :: according to WAYBEL_0:def_2 ::_thesis: ( not x in Y or not y in Y or ex b1 being Element of the carrier of (L opp) st ( b1 in Y & b1 <= x & b1 <= y ) ) assume ( x in Y & y in Y ) ; ::_thesis: ex b1 being Element of the carrier of (L opp) st ( b1 in Y & b1 <= x & b1 <= y ) then consider z being Element of L such that A1: ( z in X & z >= ~ x & z >= ~ y ) by WAYBEL_0:def_1; take z ~ ; ::_thesis: ( z ~ in Y & z ~ <= x & z ~ <= y ) ~ (z ~) = z ~ ; hence ( z ~ in Y & z ~ <= x & z ~ <= y ) by A1, Th1; ::_thesis: verum end; hence x is filtered Subset of (L opp) ; ::_thesis: verum end; assume x is filtered Subset of (L opp) ; ::_thesis: x is directed Subset of L then reconsider X = x as filtered Subset of (L opp) ; reconsider Y = X as Subset of L ; Y is directed proof let x, y be Element of L; :: according to WAYBEL_0:def_1 ::_thesis: ( not x in Y or not y in Y or ex b1 being Element of the carrier of L st ( b1 in Y & x <= b1 & y <= b1 ) ) assume ( x in Y & y in Y ) ; ::_thesis: ex b1 being Element of the carrier of L st ( b1 in Y & x <= b1 & y <= b1 ) then consider z being Element of (L opp) such that A2: ( z in X & z <= x ~ & z <= y ~ ) by WAYBEL_0:def_2; take ~ z ; ::_thesis: ( ~ z in Y & x <= ~ z & y <= ~ z ) (~ z) ~ = ~ z ; hence ( ~ z in Y & x <= ~ z & y <= ~ z ) by A2, LATTICE3:9; ::_thesis: verum end; hence x is directed Subset of L ; ::_thesis: verum end; theorem :: YELLOW_7:27 for L being RelStr for x being set holds ( x is directed Subset of (L opp) iff x is filtered Subset of L ) proof let L be RelStr ; ::_thesis: for x being set holds ( x is directed Subset of (L opp) iff x is filtered Subset of L ) let x be set ; ::_thesis: ( x is directed Subset of (L opp) iff x is filtered Subset of L ) ( x is filtered Subset of L iff x is filtered Subset of ((L opp) ~) ) by WAYBEL_0:4; hence ( x is directed Subset of (L opp) iff x is filtered Subset of L ) by Th26; ::_thesis: verum end; theorem Th28: :: YELLOW_7:28 for L being RelStr for x being set holds ( x is lower Subset of L iff x is upper Subset of (L opp) ) proof let L be RelStr ; ::_thesis: for x being set holds ( x is lower Subset of L iff x is upper Subset of (L opp) ) let x be set ; ::_thesis: ( x is lower Subset of L iff x is upper Subset of (L opp) ) hereby ::_thesis: ( x is upper Subset of (L opp) implies x is lower Subset of L ) assume x is lower Subset of L ; ::_thesis: x is upper Subset of (L opp) then reconsider X = x as lower Subset of L ; reconsider Y = X as Subset of (L opp) ; Y is upper proof let x, y be Element of (L opp); :: according to WAYBEL_0:def_20 ::_thesis: ( not x in Y or not x <= y or y in Y ) assume that A1: x in Y and A2: x <= y ; ::_thesis: y in Y ~ x >= ~ y by A2, Th1; hence y in Y by A1, WAYBEL_0:def_19; ::_thesis: verum end; hence x is upper Subset of (L opp) ; ::_thesis: verum end; assume x is upper Subset of (L opp) ; ::_thesis: x is lower Subset of L then reconsider X = x as upper Subset of (L opp) ; reconsider Y = X as Subset of L ; Y is lower proof let x, y be Element of L; :: according to WAYBEL_0:def_19 ::_thesis: ( not x in Y or not y <= x or y in Y ) assume that A3: x in Y and A4: x >= y ; ::_thesis: y in Y x ~ <= y ~ by A4, LATTICE3:9; hence y in Y by A3, WAYBEL_0:def_20; ::_thesis: verum end; hence x is lower Subset of L ; ::_thesis: verum end; theorem :: YELLOW_7:29 for L being RelStr for x being set holds ( x is lower Subset of (L opp) iff x is upper Subset of L ) proof let L be RelStr ; ::_thesis: for x being set holds ( x is lower Subset of (L opp) iff x is upper Subset of L ) let x be set ; ::_thesis: ( x is lower Subset of (L opp) iff x is upper Subset of L ) ( x is upper Subset of L iff x is upper Subset of ((L opp) ~) ) by WAYBEL_0:25; hence ( x is lower Subset of (L opp) iff x is upper Subset of L ) by Th28; ::_thesis: verum end; theorem Th30: :: YELLOW_7:30 for L being RelStr holds ( L is lower-bounded iff L opp is upper-bounded ) proof let L be RelStr ; ::_thesis: ( L is lower-bounded iff L opp is upper-bounded ) thus ( L is lower-bounded implies L opp is upper-bounded ) ::_thesis: ( L opp is upper-bounded implies L is lower-bounded ) proof given x being Element of L such that A1: x is_<=_than the carrier of L ; :: according to YELLOW_0:def_4 ::_thesis: L opp is upper-bounded take x ~ ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of (L opp) is_<=_than x ~ thus the carrier of (L opp) is_<=_than x ~ by A1, Th8; ::_thesis: verum end; given x being Element of (L opp) such that A2: x is_>=_than the carrier of (L opp) ; :: according to YELLOW_0:def_5 ::_thesis: L is lower-bounded take ~ x ; :: according to YELLOW_0:def_4 ::_thesis: ~ x is_<=_than the carrier of L thus ~ x is_<=_than the carrier of L by A2, Th9; ::_thesis: verum end; theorem Th31: :: YELLOW_7:31 for L being RelStr holds ( L opp is lower-bounded iff L is upper-bounded ) proof let L be RelStr ; ::_thesis: ( L opp is lower-bounded iff L is upper-bounded ) thus ( L opp is lower-bounded implies L is upper-bounded ) ::_thesis: ( L is upper-bounded implies L opp is lower-bounded ) proof given x being Element of (L opp) such that A1: x is_<=_than the carrier of (L opp) ; :: according to YELLOW_0:def_4 ::_thesis: L is upper-bounded take ~ x ; :: according to YELLOW_0:def_5 ::_thesis: the carrier of L is_<=_than ~ x thus the carrier of L is_<=_than ~ x by A1, Th9; ::_thesis: verum end; given x being Element of L such that A2: x is_>=_than the carrier of L ; :: according to YELLOW_0:def_5 ::_thesis: L opp is lower-bounded take x ~ ; :: according to YELLOW_0:def_4 ::_thesis: x ~ is_<=_than the carrier of (L opp) thus x ~ is_<=_than the carrier of (L opp) by A2, Th8; ::_thesis: verum end; theorem :: YELLOW_7:32 for L being RelStr holds ( L is bounded iff L opp is bounded ) proof let L be RelStr ; ::_thesis: ( L is bounded iff L opp is bounded ) thus ( L is bounded implies L opp is bounded ) ::_thesis: ( L opp is bounded implies L is bounded ) proof assume ( L is lower-bounded & L is upper-bounded ) ; :: according to YELLOW_0:def_6 ::_thesis: L opp is bounded hence ( L opp is lower-bounded & L opp is upper-bounded ) by Th30, Th31; :: according to YELLOW_0:def_6 ::_thesis: verum end; assume ( L opp is lower-bounded & L opp is upper-bounded ) ; :: according to YELLOW_0:def_6 ::_thesis: L is bounded hence ( L is lower-bounded & L is upper-bounded ) by Th30, Th31; :: according to YELLOW_0:def_6 ::_thesis: verum end; theorem :: YELLOW_7:33 for L being non empty antisymmetric lower-bounded RelStr holds ( (Bottom L) ~ = Top (L opp) & ~ (Top (L opp)) = Bottom L ) by Th12, YELLOW_0:42; theorem :: YELLOW_7:34 for L being non empty antisymmetric upper-bounded RelStr holds ( (Top L) ~ = Bottom (L opp) & ~ (Bottom (L opp)) = Top L ) by Th13, YELLOW_0:43; theorem Th35: :: YELLOW_7:35 for L being bounded LATTICE for x, y being Element of L holds ( y is_a_complement_of x iff y ~ is_a_complement_of x ~ ) proof let L be bounded LATTICE; ::_thesis: for x, y being Element of L holds ( y is_a_complement_of x iff y ~ is_a_complement_of x ~ ) let x, y be Element of L; ::_thesis: ( y is_a_complement_of x iff y ~ is_a_complement_of x ~ ) hereby ::_thesis: ( y ~ is_a_complement_of x ~ implies y is_a_complement_of x ) assume A1: y is_a_complement_of x ; ::_thesis: y ~ is_a_complement_of x ~ then x "/\" y = Bottom L by WAYBEL_1:def_23; then A2: (x ~) "\/" (y ~) = (Bottom L) ~ by Th21 .= Top (L opp) by Th12, YELLOW_0:42 ; x "\/" y = Top L by A1, WAYBEL_1:def_23; then (x ~) "/\" (y ~) = (Top L) ~ by Th23 .= Bottom (L opp) by Th13, YELLOW_0:43 ; hence y ~ is_a_complement_of x ~ by A2, WAYBEL_1:def_23; ::_thesis: verum end; assume that A3: (x ~) "\/" (y ~) = Top (L opp) and A4: (x ~) "/\" (y ~) = Bottom (L opp) ; :: according to WAYBEL_1:def_23 ::_thesis: y is_a_complement_of x thus x "\/" y = (x ~) "/\" (y ~) by Th23 .= (Top L) ~ by A4, Th13, YELLOW_0:43 .= Top L ; :: according to WAYBEL_1:def_23 ::_thesis: x "/\" y = Bottom L thus x "/\" y = (x ~) "\/" (y ~) by Th21 .= (Bottom L) ~ by A3, Th12, YELLOW_0:42 .= Bottom L ; ::_thesis: verum end; theorem Th36: :: YELLOW_7:36 for L being bounded LATTICE holds ( L is complemented iff L opp is complemented ) proof let L be bounded LATTICE; ::_thesis: ( L is complemented iff L opp is complemented ) thus ( L is complemented implies L opp is complemented ) ::_thesis: ( L opp is complemented implies L is complemented ) proof assume A1: for x being Element of L ex y being Element of L st y is_a_complement_of x ; :: according to WAYBEL_1:def_24 ::_thesis: L opp is complemented let x be Element of (L opp); :: according to WAYBEL_1:def_24 ::_thesis: ex b1 being Element of the carrier of (L opp) st b1 is_a_complement_of x consider y being Element of L such that A2: y is_a_complement_of ~ x by A1; take y ~ ; ::_thesis: y ~ is_a_complement_of x (~ x) ~ = ~ x ; hence y ~ is_a_complement_of x by A2, Th35; ::_thesis: verum end; assume A3: for x being Element of (L opp) ex y being Element of (L opp) st y is_a_complement_of x ; :: according to WAYBEL_1:def_24 ::_thesis: L is complemented let x be Element of L; :: according to WAYBEL_1:def_24 ::_thesis: ex b1 being Element of the carrier of L st b1 is_a_complement_of x consider y being Element of (L opp) such that A4: y is_a_complement_of x ~ by A3; take ~ y ; ::_thesis: ~ y is_a_complement_of x (~ y) ~ = ~ y ; hence ~ y is_a_complement_of x by A4, Th35; ::_thesis: verum end; registration let L be lower-bounded RelStr ; clusterL opp -> upper-bounded ; coherence L opp is upper-bounded by Th30; end; registration let L be upper-bounded RelStr ; clusterL opp -> lower-bounded ; coherence L opp is lower-bounded by Th31; end; registration let L be bounded complemented LATTICE; clusterL opp -> complemented ; coherence L opp is complemented by Th36; end; theorem :: YELLOW_7:37 for L being Boolean LATTICE for x being Element of L holds 'not' (x ~) = 'not' x proof let L be Boolean LATTICE; ::_thesis: for x being Element of L holds 'not' (x ~) = 'not' x let x be Element of L; ::_thesis: 'not' (x ~) = 'not' x for x being Element of L holds 'not' ('not' x) = x by WAYBEL_1:87; then 'not' x is_a_complement_of x by WAYBEL_1:86; then ('not' x) ~ is_a_complement_of x ~ by Th35; hence 'not' (x ~) = 'not' x by YELLOW_5:11; ::_thesis: verum end; definition let L be non empty RelStr ; func ComplMap L -> Function of L,(L opp) means :Def1: :: YELLOW_7:def 1 for x being Element of L holds it . x = 'not' x; existence ex b1 being Function of L,(L opp) st for x being Element of L holds b1 . x = 'not' x proof deffunc H1( Element of L) -> Element of the carrier of L = 'not' \$1; consider f being Function of L,L such that A1: for x being Element of L holds f . x = H1(x) from FUNCT_2:sch_4(); reconsider f = f as Function of L,(L opp) ; take f ; ::_thesis: for x being Element of L holds f . x = 'not' x thus for x being Element of L holds f . x = 'not' x by A1; ::_thesis: verum end; correctness uniqueness for b1, b2 being Function of L,(L opp) st ( for x being Element of L holds b1 . x = 'not' x ) & ( for x being Element of L holds b2 . x = 'not' x ) holds b1 = b2; proof let f1, f2 be Function of L,(L opp); ::_thesis: ( ( for x being Element of L holds f1 . x = 'not' x ) & ( for x being Element of L holds f2 . x = 'not' x ) implies f1 = f2 ) assume A2: ( ( for x being Element of L holds f1 . x = 'not' x ) & ( for x being Element of L holds f2 . x = 'not' x ) & not f1 = f2 ) ; ::_thesis: contradiction now__::_thesis:_for_x_being_Element_of_L_holds_f1_._x_=_f2_._x let x be Element of L; ::_thesis: f1 . x = f2 . x thus f1 . x = 'not' x by A2 .= f2 . x by A2 ; ::_thesis: verum end; hence contradiction by A2, FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def1 defines ComplMap YELLOW_7:def_1_:_ for L being non empty RelStr for b2 being Function of L,(L opp) holds ( b2 = ComplMap L iff for x being Element of L holds b2 . x = 'not' x ); registration let L be Boolean LATTICE; cluster ComplMap L -> V13() ; coherence ComplMap L is one-to-one proof let a, b be Element of L; :: according to WAYBEL_1:def_1 ::_thesis: ( not (ComplMap L) . a = (ComplMap L) . b or a = b ) set f = ComplMap L; A1: 'not' ('not' a) = a by WAYBEL_1:87; ( (ComplMap L) . a = 'not' a & (ComplMap L) . b = 'not' b ) by Def1; hence ( not (ComplMap L) . a = (ComplMap L) . b or a = b ) by A1, WAYBEL_1:87; ::_thesis: verum end; end; registration let L be Boolean LATTICE; cluster ComplMap L -> isomorphic ; coherence ComplMap L is isomorphic proof set f = ComplMap L; A1: dom (ComplMap L) = the carrier of L by FUNCT_2:def_1; A2: rng (ComplMap L) = the carrier of (L opp) proof thus rng (ComplMap L) c= the carrier of (L opp) ; :: according to XBOOLE_0:def_10 ::_thesis: the carrier of (L opp) c= rng (ComplMap L) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in the carrier of (L opp) or x in rng (ComplMap L) ) assume x in the carrier of (L opp) ; ::_thesis: x in rng (ComplMap L) then reconsider x = x as Element of L ; x = 'not' ('not' x) by WAYBEL_1:87; then (ComplMap L) . ('not' x) = x by Def1; hence x in rng (ComplMap L) by A1, FUNCT_1:def_3; ::_thesis: verum end; now__::_thesis:_for_x,_y_being_Element_of_L_holds_ (_x_<=_y_iff_(ComplMap_L)_._x_<=_(ComplMap_L)_._y_) let x, y be Element of L; ::_thesis: ( x <= y iff (ComplMap L) . x <= (ComplMap L) . y ) ( (ComplMap L) . x = ('not' x) ~ & (ComplMap L) . y = ('not' y) ~ ) by Def1; then A3: ( 'not' x >= 'not' y iff (ComplMap L) . x <= (ComplMap L) . y ) by LATTICE3:9; ( x = 'not' ('not' x) & y = 'not' ('not' y) ) by WAYBEL_1:87; hence ( x <= y iff (ComplMap L) . x <= (ComplMap L) . y ) by A3, WAYBEL_1:83; ::_thesis: verum end; hence ComplMap L is isomorphic by A2, WAYBEL_0:66; ::_thesis: verum end; end; theorem :: YELLOW_7:38 for L being Boolean LATTICE holds L,L opp are_isomorphic proof let L be Boolean LATTICE; ::_thesis: L,L opp are_isomorphic take ComplMap L ; :: according to WAYBEL_1:def_8 ::_thesis: ComplMap L is isomorphic thus ComplMap L is isomorphic ; ::_thesis: verum end; theorem :: YELLOW_7:39 for S, T being non empty RelStr for f being set holds ( ( f is Function of S,T implies f is Function of (S opp),T ) & ( f is Function of (S opp),T implies f is Function of S,T ) & ( f is Function of S,T implies f is Function of S,(T opp) ) & ( f is Function of S,(T opp) implies f is Function of S,T ) & ( f is Function of S,T implies f is Function of (S opp),(T opp) ) & ( f is Function of (S opp),(T opp) implies f is Function of S,T ) ) ; theorem :: YELLOW_7:40 for S, T being non empty RelStr for f being Function of S,T for g being Function of S,(T opp) st f = g holds ( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) ) proof let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T for g being Function of S,(T opp) st f = g holds ( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) ) let f be Function of S,T; ::_thesis: for g being Function of S,(T opp) st f = g holds ( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) ) let g be Function of S,(T ~); ::_thesis: ( f = g implies ( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) ) ) assume A1: f = g ; ::_thesis: ( ( f is monotone implies g is antitone ) & ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) ) thus ( f is monotone implies g is antitone ) ::_thesis: ( ( g is antitone implies f is monotone ) & ( f is antitone implies g is monotone ) & ( g is monotone implies f is antitone ) ) proof assume A2: for x, y being Element of S st x <= y holds f . x <= f . y ; :: according to WAYBEL_1:def_2 ::_thesis: g is antitone let x, y be Element of S; :: according to WAYBEL_0:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (T ~) holds ( not b1 = g . x or not b2 = g . y or b2 <= b1 ) ) assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (T ~) holds ( not b1 = g . x or not b2 = g . y or b2 <= b1 ) then A3: f . x <= f . y by A2; ( (f . x) ~ = f . x & (f . y) ~ = f . y ) ; hence for b1, b2 being Element of the carrier of (T ~) holds ( not b1 = g . x or not b2 = g . y or b2 <= b1 ) by A1, A3, LATTICE3:9; ::_thesis: verum end; thus ( g is antitone implies f is monotone ) ::_thesis: ( f is antitone iff g is monotone ) proof assume A4: for x, y being Element of S st x <= y holds for a, b being Element of (T opp) st a = g . x & b = g . y holds a >= b ; :: according to WAYBEL_0:def_5 ::_thesis: f is monotone let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y ) assume x <= y ; ::_thesis: f . x <= f . y then A5: g . y <= g . x by A4; ( ~ (g . x) = g . x & ~ (g . y) = g . y ) ; hence f . x <= f . y by A1, A5, Th1; ::_thesis: verum end; thus ( f is antitone implies g is monotone ) ::_thesis: ( g is monotone implies f is antitone ) proof assume A6: for x, y being Element of S st x <= y holds for a, b being Element of T st a = f . x & b = f . y holds a >= b ; :: according to WAYBEL_0:def_5 ::_thesis: g is monotone let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or g . x <= g . y ) assume x <= y ; ::_thesis: g . x <= g . y then A7: f . y <= f . x by A6; ( (f . x) ~ = f . x & (f . y) ~ = f . y ) ; hence g . x <= g . y by A1, A7, LATTICE3:9; ::_thesis: verum end; thus ( g is monotone implies f is antitone ) ::_thesis: verum proof assume A8: for x, y being Element of S st x <= y holds g . x <= g . y ; :: according to WAYBEL_1:def_2 ::_thesis: f is antitone let x, y be Element of S; :: according to WAYBEL_0:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) ) assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) then A9: g . y >= g . x by A8; ( ~ (g . x) = g . x & ~ (g . y) = g . y ) ; hence for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) by A1, A9, Th1; ::_thesis: verum end; end; theorem :: YELLOW_7:41 for S, T being non empty RelStr for f being Function of S,(T opp) for g being Function of (S opp),T st f = g holds ( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) proof let S, T be non empty RelStr ; ::_thesis: for f being Function of S,(T opp) for g being Function of (S opp),T st f = g holds ( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) let f be Function of S,(T ~); ::_thesis: for g being Function of (S opp),T st f = g holds ( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) let g be Function of (S ~),T; ::_thesis: ( f = g implies ( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) ) assume A1: f = g ; ::_thesis: ( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) thus ( f is monotone implies g is monotone ) ::_thesis: ( ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) proof assume A2: for x, y being Element of S st x <= y holds f . x <= f . y ; :: according to WAYBEL_1:def_2 ::_thesis: g is monotone let x, y be Element of (S ~); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or g . x <= g . y ) assume x <= y ; ::_thesis: g . x <= g . y then ~ y <= ~ x by Th1; then A3: f . (~ y) <= f . (~ x) by A2; ( ~ (f . (~ x)) = f . (~ x) & ~ (f . (~ y)) = f . (~ y) ) ; hence g . x <= g . y by A1, A3, Th1; ::_thesis: verum end; thus ( g is monotone implies f is monotone ) ::_thesis: ( f is antitone iff g is antitone ) proof assume A4: for x, y being Element of (S opp) st x <= y holds g . x <= g . y ; :: according to WAYBEL_1:def_2 ::_thesis: f is monotone let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y ) assume x <= y ; ::_thesis: f . x <= f . y then y ~ <= x ~ by LATTICE3:9; then A5: g . (y ~) <= g . (x ~) by A4; ( (g . (x ~)) ~ = g . (x ~) & (g . (y ~)) ~ = g . (y ~) ) ; hence f . x <= f . y by A1, A5, LATTICE3:9; ::_thesis: verum end; thus ( f is antitone implies g is antitone ) ::_thesis: ( g is antitone implies f is antitone ) proof assume A6: for x, y being Element of S st x <= y holds for a, b being Element of (T ~) st a = f . x & b = f . y holds a >= b ; :: according to WAYBEL_0:def_5 ::_thesis: g is antitone let x, y be Element of (S ~); :: according to WAYBEL_0:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds ( not b1 = g . x or not b2 = g . y or b2 <= b1 ) ) assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds ( not b1 = g . x or not b2 = g . y or b2 <= b1 ) then ~ y <= ~ x by Th1; then A7: f . (~ y) >= f . (~ x) by A6; ( ~ (f . (~ x)) = f . (~ x) & ~ (f . (~ y)) = f . (~ y) ) ; hence for b1, b2 being Element of the carrier of T holds ( not b1 = g . x or not b2 = g . y or b2 <= b1 ) by A1, A7, Th1; ::_thesis: verum end; thus ( g is antitone implies f is antitone ) ::_thesis: verum proof assume A8: for x, y being Element of (S opp) st x <= y holds for a, b being Element of T st a = g . x & b = g . y holds a >= b ; :: according to WAYBEL_0:def_5 ::_thesis: f is antitone let x, y be Element of S; :: according to WAYBEL_0:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (T ~) holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) ) assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (T ~) holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) then y ~ <= x ~ by LATTICE3:9; then A9: g . (y ~) >= g . (x ~) by A8; ( (g . (x ~)) ~ = g . (x ~) & (g . (y ~)) ~ = g . (y ~) ) ; hence for b1, b2 being Element of the carrier of (T ~) holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) by A1, A9, LATTICE3:9; ::_thesis: verum end; end; theorem Th42: :: YELLOW_7:42 for S, T being non empty RelStr for f being Function of S,T for g being Function of (S opp),(T opp) st f = g holds ( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) proof let S, T be non empty RelStr ; ::_thesis: for f being Function of S,T for g being Function of (S opp),(T opp) st f = g holds ( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) let f be Function of S,T; ::_thesis: for g being Function of (S opp),(T opp) st f = g holds ( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) let g be Function of (S ~),(T ~); ::_thesis: ( f = g implies ( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) ) assume A1: f = g ; ::_thesis: ( ( f is monotone implies g is monotone ) & ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) thus ( f is monotone implies g is monotone ) ::_thesis: ( ( g is monotone implies f is monotone ) & ( f is antitone implies g is antitone ) & ( g is antitone implies f is antitone ) ) proof assume A2: for x, y being Element of S st x <= y holds f . x <= f . y ; :: according to WAYBEL_1:def_2 ::_thesis: g is monotone let x, y be Element of (S ~); :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or g . x <= g . y ) assume x <= y ; ::_thesis: g . x <= g . y then ~ y <= ~ x by Th1; then A3: f . (~ y) <= f . (~ x) by A2; ( (f . (~ x)) ~ = f . (~ x) & (f . (~ y)) ~ = f . (~ y) ) ; hence g . x <= g . y by A1, A3, LATTICE3:9; ::_thesis: verum end; thus ( g is monotone implies f is monotone ) ::_thesis: ( f is antitone iff g is antitone ) proof assume A4: for x, y being Element of (S ~) st x <= y holds g . x <= g . y ; :: according to WAYBEL_1:def_2 ::_thesis: f is monotone let x, y be Element of S; :: according to WAYBEL_1:def_2 ::_thesis: ( not x <= y or f . x <= f . y ) assume x <= y ; ::_thesis: f . x <= f . y then y ~ <= x ~ by LATTICE3:9; then A5: g . (y ~) <= g . (x ~) by A4; ( ~ (g . (x ~)) = g . (x ~) & ~ (g . (y ~)) = g . (y ~) ) ; hence f . x <= f . y by A1, A5, Th1; ::_thesis: verum end; thus ( f is antitone implies g is antitone ) ::_thesis: ( g is antitone implies f is antitone ) proof assume A6: for x, y being Element of S st x <= y holds for a, b being Element of T st a = f . x & b = f . y holds a >= b ; :: according to WAYBEL_0:def_5 ::_thesis: g is antitone let x, y be Element of (S ~); :: according to WAYBEL_0:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of (T ~) holds ( not b1 = g . x or not b2 = g . y or b2 <= b1 ) ) assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of (T ~) holds ( not b1 = g . x or not b2 = g . y or b2 <= b1 ) then ~ y <= ~ x by Th1; then A7: f . (~ y) >= f . (~ x) by A6; ( (f . (~ x)) ~ = f . (~ x) & (f . (~ y)) ~ = f . (~ y) ) ; hence for b1, b2 being Element of the carrier of (T ~) holds ( not b1 = g . x or not b2 = g . y or b2 <= b1 ) by A1, A7, LATTICE3:9; ::_thesis: verum end; thus ( g is antitone implies f is antitone ) ::_thesis: verum proof assume A8: for x, y being Element of (S opp) st x <= y holds for a, b being Element of (T opp) st a = g . x & b = g . y holds a >= b ; :: according to WAYBEL_0:def_5 ::_thesis: f is antitone let x, y be Element of S; :: according to WAYBEL_0:def_5 ::_thesis: ( not x <= y or for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) ) assume x <= y ; ::_thesis: for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) then y ~ <= x ~ by LATTICE3:9; then A9: g . (y ~) >= g . (x ~) by A8; ( ~ (g . (x ~)) = g . (x ~) & ~ (g . (y ~)) = g . (y ~) ) ; hence for b1, b2 being Element of the carrier of T holds ( not b1 = f . x or not b2 = f . y or b2 <= b1 ) by A1, A9, Th1; ::_thesis: verum end; end; theorem :: YELLOW_7:43 for S, T being non empty RelStr for f being set holds ( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) ) proof let S, T be non empty RelStr ; ::_thesis: for f being set holds ( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) ) A1: now__::_thesis:_for_S,_S1,_T,_T1_being_RelStr_st_the_carrier_of_S_=_the_carrier_of_S1_&_the_carrier_of_T_=_the_carrier_of_T1_holds_ for_a_being_Connection_of_S,T_holds_a_is_Connection_of_S1,T1 let S, S1, T, T1 be RelStr ; ::_thesis: ( the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 implies for a being Connection of S,T holds a is Connection of S1,T1 ) assume A2: ( the carrier of S = the carrier of S1 & the carrier of T = the carrier of T1 ) ; ::_thesis: for a being Connection of S,T holds a is Connection of S1,T1 let a be Connection of S,T; ::_thesis: a is Connection of S1,T1 consider f being Function of S,T, g being Function of T,S such that A3: a = [f,g] by WAYBEL_1:def_9; reconsider g = g as Function of T1,S1 by A2; reconsider f = f as Function of S1,T1 by A2; a = [f,g] by A3; hence a is Connection of S1,T1 ; ::_thesis: verum end; ( S ~ = RelStr(# the carrier of S,( the InternalRel of S ~) #) & T ~ = RelStr(# the carrier of T,( the InternalRel of T ~) #) ) ; hence for f being set holds ( ( f is Connection of S,T implies f is Connection of S ~ ,T ) & ( f is Connection of S ~ ,T implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S,T ~ ) & ( f is Connection of S,T ~ implies f is Connection of S,T ) & ( f is Connection of S,T implies f is Connection of S ~ ,T ~ ) & ( f is Connection of S ~ ,T ~ implies f is Connection of S,T ) ) by A1; ::_thesis: verum end; theorem :: YELLOW_7:44 for S, T being non empty Poset for f1 being Function of S,T for g1 being Function of T,S for f2 being Function of (S ~),(T ~) for g2 being Function of (T ~),(S ~) st f1 = f2 & g1 = g2 holds ( [f1,g1] is Galois iff [g2,f2] is Galois ) proof let S, T be non empty Poset; ::_thesis: for f1 being Function of S,T for g1 being Function of T,S for f2 being Function of (S ~),(T ~) for g2 being Function of (T ~),(S ~) st f1 = f2 & g1 = g2 holds ( [f1,g1] is Galois iff [g2,f2] is Galois ) let f1 be Function of S,T; ::_thesis: for g1 being Function of T,S for f2 being Function of (S ~),(T ~) for g2 being Function of (T ~),(S ~) st f1 = f2 & g1 = g2 holds ( [f1,g1] is Galois iff [g2,f2] is Galois ) let g1 be Function of T,S; ::_thesis: for f2 being Function of (S ~),(T ~) for g2 being Function of (T ~),(S ~) st f1 = f2 & g1 = g2 holds ( [f1,g1] is Galois iff [g2,f2] is Galois ) let f2 be Function of (S ~),(T ~); ::_thesis: for g2 being Function of (T ~),(S ~) st f1 = f2 & g1 = g2 holds ( [f1,g1] is Galois iff [g2,f2] is Galois ) let g2 be Function of (T ~),(S ~); ::_thesis: ( f1 = f2 & g1 = g2 implies ( [f1,g1] is Galois iff [g2,f2] is Galois ) ) assume that A1: f1 = f2 and A2: g1 = g2 ; ::_thesis: ( [f1,g1] is Galois iff [g2,f2] is Galois ) hereby ::_thesis: ( [g2,f2] is Galois implies [f1,g1] is Galois ) assume A3: [f1,g1] is Galois ; ::_thesis: [g2,f2] is Galois then f1 is monotone by WAYBEL_1:8; then A4: f2 is monotone by A1, Th42; A5: now__::_thesis:_for_s_being_Element_of_(S_~) for_t_being_Element_of_(T_~)_holds_ (_g2_._t_>=_s_iff_t_>=_f2_._s_) let s be Element of (S ~); ::_thesis: for t being Element of (T ~) holds ( g2 . t >= s iff t >= f2 . s ) let t be Element of (T ~); ::_thesis: ( g2 . t >= s iff t >= f2 . s ) A6: ( (f1 . (~ s)) ~ = f1 . (~ s) & (g1 . (~ t)) ~ = g1 . (~ t) ) ; ( ~ t <= f1 . (~ s) iff g1 . (~ t) <= ~ s ) by A3, WAYBEL_1:8; hence ( g2 . t >= s iff t >= f2 . s ) by A1, A2, A6, Th2; ::_thesis: verum end; g1 is monotone by A3, WAYBEL_1:8; then g2 is monotone by A2, Th42; hence [g2,f2] is Galois by A4, A5, WAYBEL_1:8; ::_thesis: verum end; assume A7: [g2,f2] is Galois ; ::_thesis: [f1,g1] is Galois then f2 is monotone by WAYBEL_1:8; then A8: f1 is monotone by A1, Th42; A9: now__::_thesis:_for_t_being_Element_of_T for_s_being_Element_of_S_holds_ (_t_<=_f1_._s_iff_g1_._t_<=_s_) let t be Element of T; ::_thesis: for s being Element of S holds ( t <= f1 . s iff g1 . t <= s ) let s be Element of S; ::_thesis: ( t <= f1 . s iff g1 . t <= s ) A10: ( ~ (f2 . (s ~)) = f2 . (s ~) & ~ (g2 . (t ~)) = g2 . (t ~) ) ; ( s ~ <= g2 . (t ~) iff f2 . (s ~) <= t ~ ) by A7, WAYBEL_1:8; hence ( t <= f1 . s iff g1 . t <= s ) by A1, A2, A10, Th2; ::_thesis: verum end; g2 is monotone by A7, WAYBEL_1:8; then g1 is monotone by A2, Th42; hence [f1,g1] is Galois by A8, A9, WAYBEL_1:8; ::_thesis: verum end; theorem Th45: :: YELLOW_7:45 for J being set for D being non empty set for K being ManySortedSet of J for F being DoubleIndexedSet of K,D holds doms F = K proof let J be set ; ::_thesis: for D being non empty set for K being ManySortedSet of J for F being DoubleIndexedSet of K,D holds doms F = K let D be non empty set ; ::_thesis: for K being ManySortedSet of J for F being DoubleIndexedSet of K,D holds doms F = K let K be ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,D holds doms F = K let F be DoubleIndexedSet of K,D; ::_thesis: doms F = K A1: dom (doms F) = F " (SubFuncs (rng F)) by FUNCT_6:def_2; A2: SubFuncs (rng F) = rng F proof thus SubFuncs (rng F) c= rng F by FUNCT_6:18; :: according to XBOOLE_0:def_10 ::_thesis: rng F c= SubFuncs (rng F) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in rng F or x in SubFuncs (rng F) ) assume A3: x in rng F ; ::_thesis: x in SubFuncs (rng F) then ex y being set st ( y in dom F & x = F . y ) by FUNCT_1:def_3; hence x in SubFuncs (rng F) by A3, FUNCT_6:def_1; ::_thesis: verum end; A4: dom F = J by PARTFUN1:def_2; A5: now__::_thesis:_for_j_being_set_st_j_in_J_holds_ (doms_F)_._j_=_K_._j let j be set ; ::_thesis: ( j in J implies (doms F) . j = K . j ) set f = F . j; assume A6: j in J ; ::_thesis: (doms F) . j = K . j then (J --> D) . j = D by FUNCOP_1:7; then A7: F . j is Function of (K . j),D by A6, PBOOLE:def_15; (doms F) . j = dom (F . j) by A4, A6, FUNCT_6:22; hence (doms F) . j = K . j by A7, FUNCT_2:def_1; ::_thesis: verum end; ( dom K = J & F " (rng F) = dom F ) by PARTFUN1:def_2, RELAT_1:134; hence doms F = K by A4, A1, A2, A5, FUNCT_1:2; ::_thesis: verum end; definition let J, D be non empty set ; let K be V8() ManySortedSet of J; let F be DoubleIndexedSet of K,D; let j be Element of J; let k be Element of K . j; :: original: .. redefine funcF .. (j,k) -> Element of D; coherence F .. (j,k) is Element of D proof ( dom (F . j) = K . j & dom F = J ) by FUNCT_2:def_1, PARTFUN1:def_2; then F .. (j,k) = (F . j) . k by FUNCT_5:38; hence F .. (j,k) is Element of D ; ::_thesis: verum end; end; theorem :: YELLOW_7:46 for L being non empty RelStr for J being set for K being ManySortedSet of J for x being set holds ( x is DoubleIndexedSet of K,L iff x is DoubleIndexedSet of K,(L opp) ) ; theorem Th47: :: YELLOW_7:47 for L being complete LATTICE for J being non empty set for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup <= Inf proof let L be complete LATTICE; ::_thesis: for J being non empty set for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup <= Inf let J be non empty set ; ::_thesis: for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup <= Inf let K be V8() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L holds Sup <= Inf let F be DoubleIndexedSet of K,L; ::_thesis: Sup <= Inf Inf is_>=_than rng (Infs ) proof let x be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not x in rng (Infs ) or x <= Inf ) assume x in rng (Infs ) ; ::_thesis: x <= Inf then consider a being Element of J such that A1: x = Inf by WAYBEL_5:14; A2: x = inf (rng (F . a)) by A1, YELLOW_2:def_6; x is_<=_than rng (Sups ) proof reconsider J9 = product (doms F) as non empty set ; let y be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not y in rng (Sups ) or x <= y ) reconsider K9 = J9 --> J as ManySortedSet of J9 ; reconsider G = Frege F as DoubleIndexedSet of K9,L ; assume y in rng (Sups ) ; ::_thesis: x <= y then consider f being Element of J9 such that A3: y = Sup by WAYBEL_5:14; reconsider f = f as Element of product (doms F) ; A4: ( dom F = J & dom (Frege F) = product (doms F) ) by PARTFUN1:def_2; then f . a in dom (F . a) by WAYBEL_5:9; then reconsider j = f . a as Element of K . a ; A5: (F . a) . j in rng ((Frege F) . f) by A4, WAYBEL_5:9; j in dom (F . a) by A4, WAYBEL_5:9; then (F . a) . j in rng (F . a) by FUNCT_1:def_3; then A6: x <= (F . a) . j by A2, YELLOW_2:22; y = sup (rng ((Frege F) . f)) by A3, YELLOW_2:def_5; then (F . a) . j <= y by A5, YELLOW_2:22; hence x <= y by A6, ORDERS_2:3; ::_thesis: verum end; then x <= inf (rng (Sups )) by YELLOW_0:33; hence x <= Inf by YELLOW_2:def_6; ::_thesis: verum end; then sup (rng (Infs )) <= Inf by YELLOW_0:32; hence Sup <= Inf by YELLOW_2:def_5; ::_thesis: verum end; theorem Th48: :: YELLOW_7:48 for L being complete LATTICE holds ( L is completely-distributive iff for J being non empty set for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup = Inf ) proof let L be complete LATTICE; ::_thesis: ( L is completely-distributive iff for J being non empty set for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup = Inf ) thus ( L is completely-distributive implies for J being non empty set for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup = Inf ) ::_thesis: ( ( for J being non empty set for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup = Inf ) implies L is completely-distributive ) proof assume that L is complete and A1: for J being non empty set for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Inf = Sup ; :: according to WAYBEL_5:def_3 ::_thesis: for J being non empty set for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup = Inf let J be non empty set ; ::_thesis: for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup = Inf let K be V8() ManySortedSet of J; ::_thesis: for F being DoubleIndexedSet of K,L holds Sup = Inf let F be DoubleIndexedSet of K,L; ::_thesis: Sup = Inf A2: Inf = Sup by A1; A3: dom K = J by PARTFUN1:def_2; A4: doms (Frege F) = (product (doms F)) --> J by Th45; A5: dom F = J by PARTFUN1:def_2; A6: doms F = K by Th45; A7: dom (Frege F) = product (doms F) by PARTFUN1:def_2; rng (Infs ) is_<=_than Sup proof reconsider J9 = product (doms (Frege F)) as non empty set ; let a be Element of L; :: according to LATTICE3:def_9 ::_thesis: ( not a in rng (Infs ) or a <= Sup ) reconsider K9 = J9 --> (product (doms F)) as ManySortedSet of J9 ; reconsider G = Frege (Frege F) as DoubleIndexedSet of K9,L ; assume a in rng (Infs ) ; ::_thesis: a <= Sup then consider g being Element of J9 such that A8: a = Inf by WAYBEL_5:14; reconsider g9 = g as Function ; deffunc H1( set ) -> set = { (f . (g9 . f)) where f is Element of product (doms F) : g9 . f = \$1 } ; A9: dom ((product (doms F)) --> J) = product (doms F) by FUNCOP_1:13; now__::_thesis:_not__for_j_being_Element_of_J_holds_(K_._j)_\_H1(j)_<>_{} defpred S1[ set , set ] means \$2 in (K . \$1) \ H1(\$1); assume A10: for j being Element of J holds (K . j) \ H1(j) <> {} ; ::_thesis: contradiction A11: now__::_thesis:_for_j_being_set_st_j_in_J_holds_ ex_k_being_set_st_S1[j,k] let j be set ; ::_thesis: ( j in J implies ex k being set st S1[j,k] ) assume j in J ; ::_thesis: ex k being set st S1[j,k] then reconsider i = j as Element of J ; set k = the Element of (K . i) \ H1(j); (K . i) \ H1(i) <> {} by A10; then the Element of (K . i) \ H1(j) in (K . i) \ H1(i) ; hence ex k being set st S1[j,k] ; ::_thesis: verum end; consider h being Function such that A12: ( dom h = J & ( for j being set st j in J holds S1[j,h . j] ) ) from CLASSES1:sch_1(A11); now__::_thesis:_for_j_being_set_st_j_in_J_holds_ h_._j_in_(doms_F)_._j let j be set ; ::_thesis: ( j in J implies h . j in (doms F) . j ) assume j in J ; ::_thesis: h . j in (doms F) . j then h . j in (K . j) \ H1(j) by A12; hence h . j in (doms F) . j by A6; ::_thesis: verum end; then reconsider h = h as Element of product (doms F) by A6, A3, A12, CARD_3:9; g9 . h in (doms (Frege F)) . h by A4, A9, CARD_3:9; then reconsider j = g9 . h as Element of J by A4, FUNCOP_1:7; ( h . (g9 . h) in H1(j) & h . j in (K . j) \ H1(j) ) by A12; hence contradiction by XBOOLE_0:def_5; ::_thesis: verum end; then consider j being Element of J such that A13: (K . j) \ H1(j) = {} ; A14: rng (F . j) c= rng (G . g) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (F . j) or z in rng (G . g) ) assume z in rng (F . j) ; ::_thesis: z in rng (G . g) then consider u being set such that A15: u in dom (F . j) and A16: z = (F . j) . u by FUNCT_1:def_3; reconsider u = u as Element of K . j by A15; u in H1(j) by A13, XBOOLE_0:def_5; then consider f being Element of product (doms F) such that A17: u = f . (g9 . f) and A18: g9 . f = j ; ( G . g = (Frege F) .. g9 & (Frege F) . f = F .. f ) by PRALG_2:def_2; then (G . g) . f = (F .. f) . j by A7, A18, PRALG_1:def_17; then A19: (G . g) . f = z by A5, A16, A17, A18, PRALG_1:def_17; ( dom (G . g) = K9 . g & K9 . g = product (doms F) ) by FUNCOP_1:7, FUNCT_2:def_1; hence z in rng (G . g) by A19, FUNCT_1:def_3; ::_thesis: verum end; ( ex_inf_of rng (G . g),L & ex_inf_of rng (F . j),L ) by YELLOW_0:17; then inf (rng (G . g)) <= inf (rng (F . j)) by A14, YELLOW_0:35; then a <= inf (rng (F . j)) by A8, YELLOW_2:def_6; then A20: a <= Inf by YELLOW_2:def_6; Inf in rng (Infs ) by WAYBEL_5:14; then Inf <= sup (rng (Infs )) by YELLOW_2:22; then a <= sup (rng (Infs )) by A20, ORDERS_2:3; hence a <= Sup by YELLOW_2:def_5; ::_thesis: verum end; then sup (rng (Infs )) <= Sup by YELLOW_0:32; then A21: Sup <= Sup by YELLOW_2:def_5; Sup <= Inf by Th47; hence Sup = Inf by A2, A21, ORDERS_2:2; ::_thesis: verum end; assume A22: for J being non empty set for K being V8() ManySortedSet of J for F being DoubleIndexedSet of K,L holds Sup = Inf ; ::_thesis: L is completely-distributive thus L is complete ; :: according to WAYBEL_5:def_3 ::_thesis: for b1 being set for b2 being set for b3 being ManySortedFunction of b2,b1 --> the carrier of L holds //\ ((\// (b3,L)),L) = \\/ ((/\\ ((Frege b3),L)),L) let J be non empty set ; ::_thesis: for b1 being set for b2 being ManySortedFunction of b1,J --> the carrier of L holds //\ ((\// (b2,L)),L) = \\/ ((/\\ ((Frege b2),L)),L) let K be V8() ManySortedSet of J; ::_thesis: for b1 being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b1,L)),L) = \\/ ((/\\ ((Frege b1),L)),L) let F be DoubleIndexedSet of K,L; ::_thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L) A23: dom K = J by PARTFUN1:def_2; A24: doms (Frege F) = (product (doms F)) --> J by Th45; A25: dom F = J by PARTFUN1:def_2; A26: doms F = K by Th45; A27: dom (Frege F) = product (doms F) by PARTFUN1:def_2; rng (Sups ) is_>=_than Inf proof reconsider J9 = product (doms (Frege F)) as non empty set ; let a be Element of L; :: according to LATTICE3:def_8 ::_thesis: ( not a in rng (Sups ) or Inf <= a ) reconsider K9 = J9 --> (product (doms F)) as ManySortedSet of J9 ; reconsider G = Frege (Frege F) as DoubleIndexedSet of K9,L ; assume a in rng (Sups ) ; ::_thesis: Inf <= a then consider g being Element of J9 such that A28: a = Sup by WAYBEL_5:14; reconsider g9 = g as Function ; deffunc H1( set ) -> set = { (f . (g9 . f)) where f is Element of product (doms F) : g9 . f = \$1 } ; A29: dom ((product (doms F)) --> J) = product (doms F) by FUNCOP_1:13; now__::_thesis:_not__for_j_being_Element_of_J_holds_(K_._j)_\_H1(j)_<>_{} defpred S1[ set , set ] means \$2 in (K . \$1) \ H1(\$1); assume A30: for j being Element of J holds (K . j) \ H1(j) <> {} ; ::_thesis: contradiction A31: now__::_thesis:_for_j_being_set_st_j_in_J_holds_ ex_k_being_set_st_S1[j,k] let j be set ; ::_thesis: ( j in J implies ex k being set st S1[j,k] ) assume j in J ; ::_thesis: ex k being set st S1[j,k] then reconsider i = j as Element of J ; set k = the Element of (K . i) \ H1(j); (K . i) \ H1(i) <> {} by A30; then the Element of (K . i) \ H1(j) in (K . i) \ H1(i) ; hence ex k being set st S1[j,k] ; ::_thesis: verum end; consider h being Function such that A32: ( dom h = J & ( for j being set st j in J holds S1[j,h . j] ) ) from CLASSES1:sch_1(A31); now__::_thesis:_for_j_being_set_st_j_in_J_holds_ h_._j_in_(doms_F)_._j let j be set ; ::_thesis: ( j in J implies h . j in (doms F) . j ) assume j in J ; ::_thesis: h . j in (doms F) . j then h . j in (K . j) \ H1(j) by A32; hence h . j in (doms F) . j by A26; ::_thesis: verum end; then reconsider h = h as Element of product (doms F) by A26, A23, A32, CARD_3:9; g9 . h in (doms (Frege F)) . h by A24, A29, CARD_3:9; then reconsider j = g9 . h as Element of J by A24, FUNCOP_1:7; ( h . (g9 . h) in H1(j) & h . j in (K . j) \ H1(j) ) by A32; hence contradiction by XBOOLE_0:def_5; ::_thesis: verum end; then consider j being Element of J such that A33: (K . j) \ H1(j) = {} ; A34: rng (F . j) c= rng (G . g) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in rng (F . j) or z in rng (G . g) ) assume z in rng (F . j) ; ::_thesis: z in rng (G . g) then consider u being set such that A35: u in dom (F . j) and A36: z = (F . j) . u by FUNCT_1:def_3; reconsider u = u as Element of K . j by A35; u in H1(j) by A33, XBOOLE_0:def_5; then consider f being Element of product (doms F) such that A37: u = f . (g9 . f) and A38: g9 . f = j ; ( G . g = (Frege F) .. g9 & (Frege F) . f = F .. f ) by PRALG_2:def_2; then (G . g) . f = (F .. f) . j by A27, A38, PRALG_1:def_17; then A39: (G . g) . f = z by A25, A36, A37, A38, PRALG_1:def_17; ( dom (G . g) = K9 . g & K9 . g = product (doms F) ) by FUNCOP_1:7, FUNCT_2:def_1; hence z in rng (G . g) by A39, FUNCT_1:def_3; ::_thesis: verum end; ( ex_sup_of rng (G . g),L & ex_sup_of rng (F . j),L ) by YELLOW_0:17; then sup (rng (G . g)) >= sup (rng (F . j)) by A34, YELLOW_0:34; then a >= sup (rng (F . j)) by A28, YELLOW_2:def_5; then A40: a >= Sup by YELLOW_2:def_5; Sup in rng (Sups ) by WAYBEL_5:14; then Sup >= inf (rng (Sups )) by YELLOW_2:22; then a >= inf (rng (Sups )) by A40, ORDERS_2:3; hence Inf <= a by YELLOW_2:def_6; ::_thesis: verum end; then inf (rng (Sups )) >= Inf by YELLOW_0:33; then A41: Inf >= Inf by YELLOW_2:def_6; ( Inf >= Sup & Sup = Inf ) by A22, WAYBEL_5:16; hence //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L) by A41, ORDERS_2:2; ::_thesis: verum end; theorem Th49: :: YELLOW_7:49 for L being non empty antisymmetric complete RelStr for F being Function holds ( \\/ (F,L) = //\ (F,(L opp)) & //\ (F,L) = \\/ (F,(L opp)) ) proof let L be non empty antisymmetric complete RelStr ; ::_thesis: for F being Function holds ( \\/ (F,L) = //\ (F,(L opp)) & //\ (F,L) = \\/ (F,(L opp)) ) let F be Function; ::_thesis: ( \\/ (F,L) = //\ (F,(L opp)) & //\ (F,L) = \\/ (F,(L opp)) ) A1: ex_sup_of rng F,L by YELLOW_0:17; thus \\/ (F,L) = "\/" ((rng F),L) by YELLOW_2:def_5 .= "/\" ((rng F),(L opp)) by A1, Th12 .= //\ (F,(L opp)) by YELLOW_2:def_6 ; ::_thesis: //\ (F,L) = \\/ (F,(L opp)) A2: ex_inf_of rng F,L by YELLOW_0:17; thus //\ (F,L) = "/\" ((rng F),L) by YELLOW_2:def_6 .= "\/" ((rng F),(L opp)) by A2, Th13 .= \\/ (F,(L opp)) by YELLOW_2:def_5 ; ::_thesis: verum end; theorem Th50: :: YELLOW_7:50 for L being non empty antisymmetric complete RelStr for F being Function-yielding Function holds ( \// (F,L) = /\\ (F,(L opp)) & /\\ (F,L) = \// (F,(L opp)) ) proof let L be non empty antisymmetric complete RelStr ; ::_thesis: for F being Function-yielding Function holds ( \// (F,L) = /\\ (F,(L opp)) & /\\ (F,L) = \// (F,(L opp)) ) let F be Function-yielding Function; ::_thesis: ( \// (F,L) = /\\ (F,(L opp)) & /\\ (F,L) = \// (F,(L opp)) ) A1: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_ (\//_(F,L))_._x_=_(/\\_(F,(L_opp)))_._x let x be set ; ::_thesis: ( x in dom F implies (\// (F,L)) . x = (/\\ (F,(L opp))) . x ) assume x in dom F ; ::_thesis: (\// (F,L)) . x = (/\\ (F,(L opp))) . x then ( (\// (F,L)) . x = \\/ ((F . x),L) & (/\\ (F,(L opp))) . x = //\ ((F . x),(L opp)) ) by WAYBEL_5:def_1, WAYBEL_5:def_2; hence (\// (F,L)) . x = (/\\ (F,(L opp))) . x by Th49; ::_thesis: verum end; ( dom (\// (F,L)) = dom F & dom (/\\ (F,(L opp))) = dom F ) by FUNCT_2:def_1; hence \// (F,L) = /\\ (F,(L opp)) by A1, FUNCT_1:2; ::_thesis: /\\ (F,L) = \// (F,(L opp)) A2: now__::_thesis:_for_x_being_set_st_x_in_dom_F_holds_ (/\\_(F,L))_._x_=_(\//_(F,(L_opp)))_._x let x be set ; ::_thesis: ( x in dom F implies (/\\ (F,L)) . x = (\// (F,(L opp))) . x ) assume x in dom F ; ::_thesis: (/\\ (F,L)) . x = (\// (F,(L opp))) . x then ( (/\\ (F,L)) . x = //\ ((F . x),L) & (\// (F,(L opp))) . x = \\/ ((F . x),(L opp)) ) by WAYBEL_5:def_1, WAYBEL_5:def_2; hence (/\\ (F,L)) . x = (\// (F,(L opp))) . x by Th49; ::_thesis: verum end; ( dom (/\\ (F,L)) = dom F & dom (\// (F,(L opp))) = dom F ) by FUNCT_2:def_1; hence /\\ (F,L) = \// (F,(L opp)) by A2, FUNCT_1:2; ::_thesis: verum end; registration cluster non empty completely-distributive -> non empty complete for RelStr ; coherence for b1 being non empty RelStr st b1 is completely-distributive holds b1 is complete by WAYBEL_5:def_3; end; registration cluster non empty V45() finite 1 -element strict reflexive transitive antisymmetric with_suprema with_infima complete lower-bounded upper-bounded bounded connected up-complete /\-complete distributive V222() completely-distributive for RelStr ; existence ex b1 being 1 -element Poset st ( b1 is completely-distributive & b1 is strict ) proof set R = the 1 -element strict Poset; take the 1 -element strict Poset ; ::_thesis: ( the 1 -element strict Poset is completely-distributive & the 1 -element strict Poset is strict ) thus ( the 1 -element strict Poset is completely-distributive & the 1 -element strict Poset is strict ) ; ::_thesis: verum end; end; theorem :: YELLOW_7:51 for L being non empty Poset holds ( L is completely-distributive iff L opp is completely-distributive ) proof let L be non empty Poset; ::_thesis: ( L is completely-distributive iff L opp is completely-distributive ) thus ( L is completely-distributive implies L opp is completely-distributive ) ::_thesis: ( L opp is completely-distributive implies L is completely-distributive ) proof assume A1: L is completely-distributive ; ::_thesis: L opp is completely-distributive hence L opp is complete ; :: according to WAYBEL_5:def_3 ::_thesis: for b1 being set for b2 being set for b3 being ManySortedFunction of b2,b1 --> the carrier of (L opp) holds //\ ((\// (b3,(L opp))),(L opp)) = \\/ ((/\\ ((Frege b3),(L opp))),(L opp)) let J be non empty set ; ::_thesis: for b1 being set for b2 being ManySortedFunction of b1,J --> the carrier of (L opp) holds //\ ((\// (b2,(L opp))),(L opp)) = \\/ ((/\\ ((Frege b2),(L opp))),(L opp)) let K be V8() ManySortedSet of J; ::_thesis: for b1 being ManySortedFunction of K,J --> the carrier of (L opp) holds //\ ((\// (b1,(L opp))),(L opp)) = \\/ ((/\\ ((Frege b1),(L opp))),(L opp)) let F be DoubleIndexedSet of K,(L opp); ::_thesis: //\ ((\// (F,(L opp))),(L opp)) = \\/ ((/\\ ((Frege F),(L opp))),(L opp)) reconsider G = F as DoubleIndexedSet of K,L ; thus Inf = \\/ ((Sups ),L) by A1, Th49 .= Sup by A1, Th50 .= Inf by A1, Th48 .= //\ ((Infs ),L) by A1, Th50 .= Sup by A1, Th49 ; ::_thesis: verum end; assume A2: L opp is completely-distributive ; ::_thesis: L is completely-distributive then A3: L is non empty complete Poset by Th17; thus L is complete by A2, Th17; :: according to WAYBEL_5:def_3 ::_thesis: for b1 being set for b2 being set for b3 being ManySortedFunction of b2,b1 --> the carrier of L holds //\ ((\// (b3,L)),L) = \\/ ((/\\ ((Frege b3),L)),L) let J be non empty set ; ::_thesis: for b1 being set for b2 being ManySortedFunction of b1,J --> the carrier of L holds //\ ((\// (b2,L)),L) = \\/ ((/\\ ((Frege b2),L)),L) let K be V8() ManySortedSet of J; ::_thesis: for b1 being ManySortedFunction of K,J --> the carrier of L holds //\ ((\// (b1,L)),L) = \\/ ((/\\ ((Frege b1),L)),L) let F be DoubleIndexedSet of K,L; ::_thesis: //\ ((\// (F,L)),L) = \\/ ((/\\ ((Frege F),L)),L) reconsider G = F as DoubleIndexedSet of K,(L opp) ; thus Inf = \\/ ((Sups ),(L opp)) by A3, Th49 .= Sup by A3, Th50 .= Inf by A2, Th48 .= //\ ((Infs ),(L opp)) by A3, Th50 .= Sup by A3, Th49 ; ::_thesis: verum end;