let L be complete LATTICE; :: thesis: for X, Y being set st X c= Y holds
( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) )
let X, Y be set ; :: thesis: ( X c= Y implies ( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) ) )
A1: ( ex_inf_of X,L & ex_inf_of Y,L ) by YELLOW_0:17;
( ex_sup_of X,L & ex_sup_of Y,L ) by YELLOW_0:17;
hence ( X c= Y implies ( "\/" (X,L) <= "\/" (Y,L) & "/\" (X,L) >= "/\" (Y,L) ) ) by A1, YELLOW_0:34, YELLOW_0:35; :: thesis: verum