theorem :: WAYBEL_4:46
for L being complete LATTICE holds
( L is continuous iff ( L is meet-continuous & ex R being auxiliary approximating Relation of L st
for R9 being auxiliary approximating Relation of L holds R c= R9 ) )