let x, y be set ; ( 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 Th68;
x in {x}
by TARSKI:def 1;
then
the_rank_of x in the_rank_of {x}
by Th68;
hence
the_rank_of x in the_rank_of [x,y]
by A1, ORDINAL1:10; 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 Th68;
y in {x,y}
by TARSKI:def 2;
then
the_rank_of y in the_rank_of {x,y}
by Th68;
hence
the_rank_of y in the_rank_of [x,y]
by A2, ORDINAL1:10; verum