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:10;
then A7: B c= A by ORDINAL1:def 2;
A8: Rank (succ B) = bool (Rank B) by Lm2;
then A9: not Rank B, Rank A are_equipotent by A5, CARD_1:29;
Rank B c= Rank A by A7, Th43;
hence not X, Rank A are_equipotent by A3, A5, A8, A9, CARD_1:44; :: thesis: verum

end;

now

assume that
A12: A <> {} and
A13: for B being Ordinal holds A <> succ B ; :: thesis: not X, Rank A are_equipotent
A is limit_ordinal by A13, ORDINAL1:42;
then consider B being Ordinal such that
A15: B in A and
A16: X in Rank B by A3, A12, Th35;
A17: Rank B in Rank A by A15, Th42;
A18: ( not X, Rank B are_equipotent & X c= Rank B ) by A2, A15, A16, ORDINAL1:def 2;
Rank B c= Rank A by A17, ORDINAL1:def 2;
hence not X, Rank A are_equipotent by A18, CARD_1:44; :: thesis: verum

end;

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

end;

A20: 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 A21: X in Rank A ; :: thesis: ( not X, Rank A are_equipotent & card X in card (Rank A) )
then A22: X c= Rank A by ORDINAL1:def 2;
A23: not X, Rank A are_equipotent by A20, A21;
A24: card X c= card (Rank A) by A22, CARD_1:27;
card X <> card (Rank A) by A23, CARD_1:21;
hence ( not X, Rank A are_equipotent & card X in card (Rank A) ) by A20, A21, A24, CARD_1:13; :: thesis: verum