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 that
A1: X c= Y and
A2: ex_sup_of X,L and
A3: 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 A4: x in X ; :: thesis: x <= "\/" (Y,L)
"\/" (Y,L) is_>=_than Y by A3, Def9;
hence x <= "\/" (Y,L) by A1, A4; :: thesis: verum
end;
hence "\/" (X,L) <= "\/" (Y,L) by A2, Def9; :: thesis: verum