defpred S₁[ Ordinal] means for X being set st X in Rank $1 holds
not X, Rank $1 are_equipotent ;
A1: for A being Ordinal st ( for B being Ordinal st B in A holds
S₁[B] ) holds
S₁[A]

proof

let A be Ordinal; :: thesis: ( ( for B being Ordinal st B in A holds
S₁[B] ) implies S₁[A] )
assume A2: for B being Ordinal st B in A holds
S₁[B] ; :: thesis: S₁[A]
let X be set ; :: thesis: ( X in Rank A implies not X, Rank A are_equipotent )
assume A3: X in Rank A ; :: thesis: not X, Rank A are_equipotent

A4: now :: thesis: ( ex B being Ordinal st A = succ B implies not X, Rank A are_equipotent )

given B being Ordinal such that A5: A = succ B ; :: thesis: not X, Rank A are_equipotent
A6: B c= A by A5, ORDINAL1:6, ORDINAL1:def 2;
A7: Rank (succ B) = bool (Rank B) by Lm2;
then A8: not Rank B, Rank A are_equipotent by A5, CARD_1:13;
Rank B c= Rank A by A6, Th37;
hence not X, Rank A are_equipotent by A3, A5, A7, A8, CARD_1:24; :: thesis: verum

end;

now :: thesis: ( A <> {} & ( for B being Ordinal holds A <> succ B ) implies not X, Rank A are_equipotent )

assume that
A9: A <> {} and
A10: for B being Ordinal holds A <> succ B ; :: thesis: not X, Rank A are_equipotent
A is limit_ordinal by A10, ORDINAL1:29;
then consider B being Ordinal such that
A11: B in A and
A12: X in Rank B by A3, A9, Th31;
A13: ( not X, Rank B are_equipotent & X c= Rank B ) by A2, A11, A12, ORDINAL1:def 2;
Rank B c= Rank A by A11, Th36, ORDINAL1:def 2;
hence not X, Rank A are_equipotent by A13, CARD_1:24; :: thesis: verum

end;

hence not X, Rank A are_equipotent by A3, A4, Lm2; :: thesis: verum

end;

A14: for A being Ordinal holds S₁[A] from ORDINAL1:sch 2(A1);
let A be Ordinal; :: thesis: for X being set st X in Rank A holds
( not X, Rank A are_equipotent & card X in card (Rank A) )
let X be set ; :: thesis: ( X in Rank A implies ( not X, Rank A are_equipotent & card X in card (Rank A) ) )
assume A15: X in Rank A ; :: thesis: ( not X, Rank A are_equipotent & card X in card (Rank A) )
A16: card X c= card (Rank A) by A15, CARD_1:11, ORDINAL1:def 2;
card X <> card (Rank A) by A14, A15, CARD_1:5;
hence ( not X, Rank A are_equipotent & card X in card (Rank A) ) by A14, A15, A16, CARD_1:3; :: thesis: verum