let x be set ; :: thesis: for A being Ordinal holds
( x in Rank A iff {x} in Rank (succ A) )
let A be Ordinal; :: thesis: ( x in Rank A iff {x} in Rank (succ A) )
A1: ( x in Rank A iff {x} c= Rank A ) by ZFMISC_1:37;
thus ( x in Rank A iff {x} in Rank (succ A) ) by A1, Th36; :: thesis: verum