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

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