let C be complete Lattice; :: thesis: for a being Element of C
for X being set st a is_less_than X holds
a [= "/\" (X,C)
let a be Element of C; :: thesis: for X being set st a is_less_than X holds
a [= "/\" (X,C)
let X be set ; :: thesis: ( a is_less_than X implies a [= "/\" (X,C) )
assume a is_less_than X ; :: thesis: a [= "/\" (X,C)
then a in { b where b is Element of C : b is_less_than X } ;
hence a [= "/\" (X,C) by Th38; :: thesis: verum