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; :: 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; :: thesis: verum

end;

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