set X = the set ;
take R = bool the set ; :: thesis: R includes_lattice_of R
let a, b be set ; :: according to COHSP_1:def 7 :: 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= the set by A1, XBOOLE_1:108;
hence a /\ b in R ; :: thesis: a \/ b in R
a \/ b c= the set by A1, A2, XBOOLE_1:8;
hence a \/ b in R ; :: thesis: verum