theorem :: WAYBEL30:39

for N being complete Lawson meet-continuous TopLattice holds
( N is continuous iff for x being Element of N holds x = "\/" ( { (inf V) where V is Subset of N : ( x in V & V in lambda N ) } ,N) )