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