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 that
A1: a in R and
A2: b in R ; :: thesis: ( a /\ b in R & a \/ b in R )
a /\ b c= X by A1, XBOOLE_1:108;
hence a /\ b in R ; :: thesis: a \/ b in R
a \/ b c= X by A1, A2, XBOOLE_1:8;
hence a \/ b in R ; :: thesis: verum