let X, x, y be set ; :: thesis: ( X includes_lattice_of x,y iff ( x in X & y in X & x /\ y in X & x \/ y in X ) )
thus ( X includes_lattice_of x,y implies ( x in X & y in X & x /\ y in X & x \/ y in X ) ) :: thesis: ( x in X & y in X & x /\ y in X & x \/ y in X implies X includes_lattice_of x,y )

proof

assume A1: for a, b being set st a in {x,y} & b in {x,y} holds
( a /\ b in X & a \/ b in X ) ; :: according to COHSP_1:def 8,COHSP_1:def 9 :: thesis: ( x in X & y in X & x /\ y in X & x \/ y in X )
( x in {x,y} & y in {x,y} & x \/ x = x & y \/ y = y ) by TARSKI:def 2;
hence ( x in X & y in X & x /\ y in X & x \/ y in X ) by A1; :: thesis: verum

end;

assume A2: ( x in X & y in X & x /\ y in X & x \/ y in X ) ; :: thesis: X includes_lattice_of x,y
let a, b be set ; :: according to COHSP_1:def 8,COHSP_1:def 9 :: thesis: ( a in {x,y} & b in {x,y} implies ( a /\ b in X & a \/ b in X ) )
assume ( a in {x,y} & b in {x,y} ) ; :: thesis: ( a /\ b in X & a \/ b in X )
then ( ( a = x or a = y ) & ( b = x or b = y ) & x \/ x = x & y \/ y = y & x /\ x = x & y /\ y = y ) by TARSKI:def 2;
hence ( a /\ b in X & a \/ b in X ) by A2; :: thesis: verum