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