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