let y, X, A be set ; :: thesis: ( not y in proj2 X implies [:A,{y}:] misses X )
set X2 = proj2 X;
set Y = [:A,{y}:];
set Z = X /\ [:A,{y}:];
assume B0: not y in proj2 X ; :: thesis: [:A,{y}:] misses X
assume [:A,{y}:] meets X ; :: thesis: contradiction
then X /\ [:A,{y}:] <> {} by XBOOLE_0:def 7;
then consider z being set such that
B1: z in X /\ [:A,{y}:] by XBOOLE_0:def 1;
set x1 = z `1 ;
set y1 = z `2 ;
( z `1 in A & z `2 in {y} & z = [(z `1),(z `2)] & z in X ) by B1, MCART_1:10, MCART_1:21;
then ( z `2 = y & z `2 in proj2 X ) by RELAT_1:def 5, TARSKI:def 1;
hence contradiction by B0; :: thesis: verum