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