let X be set ; :: thesis: for U being Grothendieck st X in U holds
Rrank X in U

let U be Grothendieck; :: thesis: ( X in U implies Rrank X in U )
defpred S1[ Ordinal] means for A being set st the_rank_of A in \$1 & A in U holds
Rrank A 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: ( the_rank_of S in A & S in U implies Rrank S in U )
assume A3: ( the_rank_of S in A & S in U ) ; :: thesis: Rrank S in U
deffunc H1( object ) -> Element of K28(K28((Rrank \$1))) = bool (Rrank \$1);
consider v being Function such that
A4: ( dom v = S & ( for x being object st x in S holds
v . x = H1(x) ) ) from A5: rng v c= U
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng v or y in U )
assume A6: y in rng v ; :: thesis: y in U
consider x being object such that
A7: ( x in dom v & v . x = y ) by ;
succ () c= the_rank_of S by ;
then A8: for S being set st the_rank_of S in succ () & S in U holds
Rrank S in U by A2, A3;
A9: x in U by A3, Th13, A7, A4;
Rrank x in U by ;
then bool () in U by Def1;
hence y in U by A7, A4; :: thesis: verum
end;
A10: union (rng v) c= Rrank S
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in union (rng v) or a in Rrank S )
assume a in union (rng v) ; :: thesis: a in Rrank S
then consider b being set such that
A11: ( a in b & b in rng v ) by TARSKI:def 4;
consider x being object such that
A12: ( x in dom v & v . x = b ) by ;
reconsider a = a, b = b, x = x as set by TARSKI:1;
b = bool () by ;
hence a in Rrank S by A11, A12, A4, Th4; :: thesis: verum
end;
Rrank S c= union (rng v)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Rrank S or x in union (rng v) )
assume x in Rrank S ; :: thesis: x in union (rng v)
then consider a being set such that
A13: ( a in S & x in bool () ) by Th4;
( v . a = bool () & v . a in rng v ) by ;
hence x in union (rng v) by ; :: thesis: verum
end;
then union (rng v) = Rrank S by A10;
hence Rrank S in U by A5, A4, A3, Def3; :: thesis: verum
end;
A14: for O being Ordinal holds S1[O] from the_rank_of X in succ () by ORDINAL1:6;
hence ( X in U implies Rrank X in U ) by A14; :: thesis: verum