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)) )
A1: ( x in Rank A iff {x} in Rank (succ A) ) by Th49;
A2: ( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) ) by Th50;
thus ( ( x in Rank A & y in Rank A ) iff [x,y] in Rank (succ (succ A)) ) by A1, A2, Th50; :: thesis: verum