let A, X, y 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 A1: not y in proj2 X ; :: thesis: [:A,{y}:] misses X
assume [:A,{y}:] meets X ; :: thesis: contradiction
then X /\ [:A,{y}:] <> {} ;
then consider z being object such that
A2: z in X /\ [:A,{y}:] ;
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 A2, MCART_1:10, MCART_1:21;
then ( z `2 = y & z `2 in proj2 X ) by TARSKI:def 1, XTUPLE_0:def 13;
hence contradiction by A1; :: thesis: verum