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