let X be set ; :: thesis: for L being complete LATTICE
for a being Element of L st a in X holds
( a <= "\/" X,L & "/\" X,L <= a )
let L be complete LATTICE; :: thesis: for a being Element of L st a in X holds
( a <= "\/" X,L & "/\" X,L <= a )
let a be Element of L; :: thesis: ( a in X implies ( a <= "\/" X,L & "/\" X,L <= a ) )
assume A1: a in X ; :: thesis: ( a <= "\/" X,L & "/\" X,L <= a )
X is_<=_than "\/" X,L by YELLOW_0:32;
hence a <= "\/" X,L by A1, LATTICE3:def 9; :: thesis: "/\" X,L <= a
X is_>=_than "/\" X,L by YELLOW_0:33;
hence "/\" X,L <= a by A1, LATTICE3:def 8; :: thesis: verum