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, Th39;
hence "/\" (X,C) = a by A3, LATTICES:8; :: thesis: verum