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 that
A1: a in X and
A2: a is_less_than X ; :: thesis: "/\" X,C = a
A3: "/\" X,C [= a by A1, Th38;
a [= "/\" X,C by A2, Th40;
hence "/\" X,C = a by A3, LATTICES:26; :: thesis: verum