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 A) )
let A be Ordinal; :: thesis: ( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) )
( ( x in Rank A & y in Rank A implies {x,y} c= Rank A ) & ( {x,y} c= Rank A implies ( x in Rank A & y in Rank A ) ) & ( {x,y} c= Rank A implies {x,y} in Rank (succ A) ) & ( {x,y} in Rank (succ A) implies {x,y} c= Rank A ) ) by Th36, ZFMISC_1:38;
hence ( ( x in Rank A & y in Rank A ) iff {x,y} in Rank (succ A) ) ; :: thesis: verum