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 ( ex_sup_of X,L or ex_inf_of X,L opp ) ; :: thesis: "\/" X,L = "/\" X,(L opp )
then A1: ( ex_sup_of X,L & ex_inf_of X,L opp ) by Th10;
then "\/" X,L is_>=_than X by YELLOW_0:def 9;
then A2: ("\/" X,L) ~ is_<=_than X by Th8;

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 A1, YELLOW_0:def 9;
hence x <= ("\/" X,L) ~ by Th2; :: thesis: verum

end;

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