let x, y be object ; :: thesis: ( the_rank_of x in the_rank_of [x,y] & the_rank_of y in the_rank_of [x,y] )
{x} in {{x,y},{x}} by TARSKI:def 2;
then A1: the_rank_of {x} in the_rank_of {{x,y},{x}} by CLASSES1:68;
x in {x} by TARSKI:def 1;
then the_rank_of x in the_rank_of {x} by CLASSES1:68;
hence the_rank_of x in the_rank_of [x,y] by A1, ORDINAL1:10; :: thesis: the_rank_of y in the_rank_of [x,y]
{x,y} in {{x,y},{x}} by TARSKI:def 2;
then A2: the_rank_of {x,y} in the_rank_of {{x,y},{x}} by CLASSES1:68;
y in {x,y} by TARSKI:def 2;
then the_rank_of y in the_rank_of {x,y} by CLASSES1:68;
hence the_rank_of y in the_rank_of [x,y] by A2, ORDINAL1:10; :: thesis: verum