let C, A, B be Ordinal; :: thesis: ( 1 in C & A in B implies exp C,A in exp C,B )
defpred S₁[ Ordinal] means for A being Ordinal st A in $1 holds
exp C,A in exp C,$1;
A1: for B being Ordinal st B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S₁[D] ) holds
S₁[B]

proof

deffunc H₁( Ordinal) -> set = exp C,$1;
let B be Ordinal; :: thesis: ( B <> {} & B is limit_ordinal & ( for D being Ordinal st D in B holds
S₁[D] ) implies S₁[B] )
assume that
A2: B <> {} and
A3: B is limit_ordinal and
A4: for D being Ordinal st D in B holds
S₁[D] ; :: thesis: S₁[B]
consider fi being Ordinal-Sequence such that
A5: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
fi is increasing

proof

let B1, B2 be Ordinal; :: according to ORDINAL2:def 16 :: thesis: ( not B1 in B2 or not B2 in proj1 fi or fi . B1 in fi . B2 )
assume that
A6: B1 in B2 and
A7: B2 in dom fi ; :: thesis: fi . B1 in fi . B2
A8: fi . B1 = exp C,B1 by A5, A6, A7, ORDINAL1:19;
exp C,B1 in exp C,B2 by A4, A5, A6, A7;
hence fi . B1 in fi . B2 by A5, A7, A8; :: thesis: verum

end;

then A9: sup fi = lim fi by A2, A3, A5, Th8;
let A be Ordinal; :: thesis: ( A in B implies exp C,A in exp C,B )
assume A10: A in B ; :: thesis: exp C,A in exp C,B
fi . A = exp C,A by A10, A5;
then A11: exp C,A in rng fi by A10, A5, FUNCT_1:def 5;
exp C,B = lim fi by A2, A3, A5, ORDINAL2:62;
hence exp C,A in exp C,B by A9, A11, ORDINAL2:27; :: thesis: verum

end;

assume A12: 1 in C ; :: thesis: ( not A in B or exp C,A in exp C,B )
A13: for B being Ordinal st S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume A14: for A being Ordinal st A in B holds
exp C,A in exp C,B ; :: thesis: S₁[ succ B]
let A be Ordinal; :: thesis: ( A in succ B implies exp C,A in exp C,(succ B) )
assume A in succ B ; :: thesis: exp C,A in exp C,(succ B)
then A15: A c= B by ORDINAL1:34;

A16: now

assume A <> B ; :: thesis: exp C,A in exp C,B
then A c< B by A15, XBOOLE_0:def 8;
hence exp C,A in exp C,B by A14, ORDINAL1:21; :: thesis: verum

end;

exp C,B in exp C,(succ B) by A12, Th23;
hence exp C,A in exp C,(succ B) by A16, ORDINAL1:19; :: thesis: verum

end;

A17: S₁[ {} ] ;
for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A17, A13, A1);
hence ( not A in B or exp C,A in exp C,B ) ; :: thesis: verum