let L be RelStr ; :: thesis: for X being set holds
( ex_sup_of X,L opp iff ex_inf_of X,L )
let X be set ; :: thesis: ( ex_sup_of X,L opp iff ex_inf_of X,L )
( ex_inf_of X,L iff ex_inf_of X,(L opp) ~ ) by YELLOW_0:14;
hence ( ex_sup_of X,L opp iff ex_inf_of X,L ) by Th10; :: thesis: verum