let x, y, z be set ; ( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] )
A1:
rng <*x,y*> = {x,y}
by FINSEQ_2:127;
then A2:
x in rng <*x,y*>
by TARSKI:def 2;
A3:
y in rng <*x,y*>
by A1, TARSKI:def 2;
A4:
the_rank_of x in the_rank_of [<*x,y*>,z]
by A2, CLASSES1:82;
the_rank_of y in the_rank_of [<*x,y*>,z]
by A3, CLASSES1:82;
hence
( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] )
by A4; verum