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

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