let C be complete Lattice; :: thesis: for a being Element of C
for X being set st a in X & a is_less_than X holds
"/\" X,C = a
let a be Element of C; :: thesis: for X being set st a in X & a is_less_than X holds
"/\" X,C = a
let X be set ; :: thesis: ( a in X & a is_less_than X implies "/\" X,C = a )
assume ( a in X & a is_less_than X ) ; :: thesis: "/\" X,C = a
then ( "/\" X,C [= a & a [= "/\" X,C ) by Th38, Th40;
hence "/\" X,C = a by LATTICES:26; :: thesis: verum