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

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