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