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

A1: ( x \/ x = x & y \/ y = y ) ;
A2: ( x in {x,y} & y in {x,y} ) by TARSKI:def 2;
assume 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 7,COHSP_1:def 8 :: thesis: ( x in X & y in X & x /\ y in X & x \/ y in X )
hence ( x in X & y in X & x /\ y in X & x \/ y in X ) by A2, A1; :: thesis: verum

end;

assume A3: ( 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 7,COHSP_1:def 8 :: thesis: ( a in {x,y} & b in {x,y} implies ( a /\ b in X & a \/ b in X ) )
assume that
A4: a in {x,y} and
A5: b in {x,y} ; :: thesis: ( a /\ b in X & a \/ b in X )
A6: ( b = x or b = y ) by A5, TARSKI:def 2;
( a = x or a = y ) by A4, TARSKI:def 2;
hence ( a /\ b in X & a \/ b in X ) by A3, A6; :: thesis: verum