consider X being set ;
take R = bool X; :: thesis: R includes_lattice_of R
let a, b be set ; :: according to COHSP_1:def 8 :: thesis: ( not a in R or not b in R or ( a /\ b in R & a \/ b in R ) )
assume A1: ( a in R & b in R ) ; :: thesis: ( a /\ b in R & a \/ b in R )
then a /\ b c= X by XBOOLE_1:108;
hence a /\ b in R ; :: thesis: a \/ b in R
a \/ b c= X by A1, XBOOLE_1:8;
hence a \/ b in R ; :: thesis: verum