let L be non empty LattStr ; :: thesis: for X being Subset of L st X is directed holds
not X is empty
let X be Subset of L; :: thesis: ( X is directed implies not X is empty )
assume for Y being finite Subset of X ex x being Element of L st
( "\/" (Y,L) [= x & x in X ) ; :: according to QUANTAL1:def 1 :: thesis: not X is empty
then ex x being Element of L st
( "\/" (({} X),L) [= x & x in X ) ;
hence not X is empty ; :: thesis: verum