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;

hence "\/" (X,L) = "/\" (X,(L opp)) by A3, A4, YELLOW_0:def 10; :: thesis: verum

"\/" (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)) ~

ex_inf_of X,L opp
by A1, Th10;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;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

hence "\/" (X,L) = "/\" (X,(L opp)) by A3, A4, YELLOW_0:def 10; :: thesis: verum