let X, x, y be set ; ( 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 ) )
( x in X & y in X & x /\ y in X & x \/ y in X implies X includes_lattice_of x,y )
assume A3:
( x in X & y in X & x /\ y in X & x \/ y in X )
; X includes_lattice_of x,y
let a, b be set ; COHSP_1:def 7,COHSP_1:def 8 ( 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}
; ( 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; verum