reconsider x99 = x, y99 = y as Subset of X by Def1;
assume that
A3: x = x9 and
A4: y = y9 ; :: thesis: x "/\" y = x9 /\ y9
thus x "/\" y = H₃( BooleLatt X) . (x99,y99)
.= x9 /\ y9 by A3, A4, Def1 ; :: thesis: verum