let C be complete Lattice; :: thesis: for X, Y being set st ( for a being Element of C st a in X holds
ex b being Element of C st
( a [= b & b in Y ) ) holds
"\/" (X,C) [= "\/" (Y,C)
let X, Y be set ; :: thesis: ( ( for a being Element of C st a in X holds
ex b being Element of C st
( a [= b & b in Y ) ) implies "\/" (X,C) [= "\/" (Y,C) )
assume A1: for a being Element of C st a in X holds
ex b being Element of C st
( a [= b & b in Y ) ; :: thesis: "\/" (X,C) [= "\/" (Y,C)
X is_less_than "\/" (Y,C)

proof

let a be Element of C; :: according to LATTICE3:def 17 :: thesis: ( a in X implies a [= "\/" (Y,C) )
assume a in X ; :: thesis: a [= "\/" (Y,C)
then consider b being Element of C such that
A2: a [= b and
A3: b in Y by A1;
b [= "\/" (Y,C) by A3, Th38;
hence a [= "\/" (Y,C) by A2, LATTICES:7; :: thesis: verum

end;

hence "\/" (X,C) [= "\/" (Y,C) by Def21; :: thesis: verum