let X be set ; :: thesis: for A being Ordinal
for U being Grothendieck st X in U & X,A are_equipotent holds
A in U

let A be Ordinal; :: thesis: for U being Grothendieck st X in U & X,A are_equipotent holds
A in U

let U be Grothendieck; :: thesis: ( X in U & X,A are_equipotent implies A in U )
defpred S1[ Ordinal] means for X being set st X,\$1 are_equipotent & X in U holds
\$1 in U;
A1: for A being Ordinal st ( for C being Ordinal st C in A holds
S1[C] ) holds
S1[A]
proof
let A be Ordinal; :: thesis: ( ( for C being Ordinal st C in A holds
S1[C] ) implies S1[A] )

assume A2: for C being Ordinal st C in A holds
S1[C] ; :: thesis: S1[A]
let S be set ; :: thesis: ( S,A are_equipotent & S in U implies A in U )
assume A3: ( S,A are_equipotent & S in U ) ; :: thesis: A in U
consider f being Function such that
A4: ( f is one-to-one & dom f = S & rng f = A ) by ;
rng f c= U
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in U )
assume A5: y in rng f ; :: thesis: y in U
reconsider B = y as Ordinal by A5, A4;
A6: B |` f is one-to-one by ;
A7: rng (B |` f) = B by ;
dom (B |` f) in U by ;
hence y in U by ; :: thesis: verum
end;
hence A in U by A4, A3, Th2; :: thesis: verum
end;
for O being Ordinal holds S1[O] from hence ( X in U & X,A are_equipotent implies A in U ) ; :: thesis: verum