let X be non empty set ; :: thesis: ( X includes_lattice_of X implies ( X is c=directed & X is c=filtered ) )
assume A1: for a, b being set st a in X & b in X holds
( a /\ b in X & a \/ b in X ) ; :: according to COHSP_1:def 7 :: thesis: ( X is c=directed & X is c=filtered )
for a, b being set st a in X & b in X holds
ex c being set st
( a \/ b c= c & c in X ) by A1;
hence X is c=directed by Th6; :: thesis: X is c=filtered
for a, b being set st a in X & b in X holds
ex c being set st
( c c= a /\ b & c in X ) by A1;
hence X is c=filtered by Th8; :: thesis: verum