let L be RelStr ; :: thesis: for X, Y being set st X c= Y & ex_sup_of X,L & ex_sup_of Y,L holds
"\/" X,L <= "\/" Y,L
let X, Y be set ; :: thesis: ( X c= Y & ex_sup_of X,L & ex_sup_of Y,L implies "\/" X,L <= "\/" Y,L )
assume A1: ( X c= Y & ex_sup_of X,L & ex_sup_of Y,L ) ; :: thesis: "\/" X,L <= "\/" Y,L
"\/" Y,L is_>=_than X

proof

let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in X or x <= "\/" Y,L )
assume x in X ; :: thesis: x <= "\/" Y,L
then ( x in Y & "\/" Y,L is_>=_than Y ) by A1, Def9;
hence x <= "\/" Y,L by LATTICE3:def 9; :: thesis: verum

end;

hence "\/" X,L <= "\/" Y,L by A1, Def9; :: thesis: verum