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