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

given B being Ordinal such that A5: A = succ B ; :: thesis: not X, Rank A are_equipotent
B in A by A5, ORDINAL1:6;
then A6: B c= A by 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, Th43;
hence not X, Rank A are_equipotent by A3, A5, A7, A8, CARD_1:24; :: thesis: verum

end;

now

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, Th35;
A13: Rank B in Rank A by A11, Th42;
A14: ( not X, Rank B are_equipotent & X c= Rank B ) by A2, A11, A12, ORDINAL1:def 2;
Rank B c= Rank A by A13, ORDINAL1:def 2;
hence not X, Rank A are_equipotent by A14, CARD_1:24; :: thesis: verum

end;

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

end;

A15: 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 A16: X in Rank A ; :: thesis: ( not X, Rank A are_equipotent & card X in card (Rank A) )
then A17: X c= Rank A by ORDINAL1:def 2;
A18: not X, Rank A are_equipotent by A15, A16;
A19: card X c= card (Rank A) by A17, CARD_1:11;
card X <> card (Rank A) by A18, CARD_1:5;
hence ( not X, Rank A are_equipotent & card X in card (Rank A) ) by A15, A16, A19, CARD_1:3; :: thesis: verum