let L be 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))
let X be set ; ( ( 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 )
; "\/" (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;
ex_inf_of X,L opp
by A1, Th10;
hence
"\/" (X,L) = "/\" (X,(L opp))
by A3, A4, YELLOW_0:def 10; verum