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 & b in Y ) by A1;
b [= "\/" Y,C by A2, Th38;
hence a [= "\/" Y,C by A2, LATTICES:25; :: thesis: verum

end;

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