let x, y, z be set ; :: thesis: ( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] )
rng <*x,y*> = {x,y} by FINSEQ_2:147;
then ( x in rng <*x,y*> & y in rng <*x,y*> ) by TARSKI:def 2;
then ( the_rank_of x in the_rank_of [<*x,y*>,z] & the_rank_of y in the_rank_of [<*x,y*>,z] ) by CLASSES1:90;
hence ( x <> [<*x,y*>,z] & y <> [<*x,y*>,z] ) ; :: thesis: verum