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; :: thesis: "/\" (X,L) <= a
X is_>=_than "/\" (X,L) by YELLOW_0:33;
hence "/\" (X,L) <= a by A1; :: thesis: verum