let C be complete Lattice; :: thesis: for a being Element of C
for X being set st a in X holds
( a [= "\/" X,C & "/\" X,C [= a )
let a be Element of C; :: thesis: for X being set st a in X holds
( a [= "\/" X,C & "/\" X,C [= a )
let X be set ; :: thesis: ( a in X implies ( a [= "\/" X,C & "/\" X,C [= a ) )
assume A1: a in X ; :: thesis: ( a [= "\/" X,C & "/\" X,C [= a )
X is_less_than "\/" X,C by Def21;
hence a [= "\/" X,C by A1, Def17; :: thesis: "/\" X,C [= a
{ b where b is Element of C : b is_less_than X } is_less_than a

proof

let c be Element of C; :: according to LATTICE3:def 17 :: thesis: ( c in { b where b is Element of C : b is_less_than X } implies c [= a )
assume c in { b where b is Element of C : b is_less_than X } ; :: thesis: c [= a
then ex b being Element of C st
( c = b & b is_less_than X ) ;
hence c [= a by A1, Def16; :: thesis: verum

end;

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