let x, y be set ; :: thesis: for A being Ordinal holds
( ( x in Rank A & y in Rank A ) iff [x,y] in Rank (succ (succ A)) )
let A be Ordinal; :: thesis: ( ( x in Rank A & y in Rank A ) iff [x,y] in Rank (succ (succ A)) )
( ( x in Rank A implies {x} in Rank (succ A) ) & ( {x} in Rank (succ A) implies x in Rank A ) & ( x in Rank A & y in Rank A implies {x,y} in Rank (succ A) ) & ( {x,y} in Rank (succ A) implies ( x in Rank A & y in Rank A ) ) & ( {x} in Rank (succ A) & {x,y} in Rank (succ A) implies {{x,y},{x}} in Rank (succ (succ A)) ) & ( {{x,y},{x}} in Rank (succ (succ A)) implies ( {x} in Rank (succ A) & {x,y} in Rank (succ A) ) ) & {{x,y},{x}} = [x,y] ) by Th49, Th50;
hence ( ( x in Rank A & y in Rank A ) iff [x,y] in Rank (succ (succ A)) ) ; :: thesis: verum