let C be complete Lattice; :: thesis: for a being Element of
for X being set st a is_less_than X holds
a [= "/\" X,C
let a be Element of ; :: 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 : b is_less_than X } ;
hence a [= "/\" X,C by Th38; :: thesis: verum