let C, A, B be Ordinal; :: thesis: ( 1 in C & A in B implies exp C,A in exp C,B )
assume A1: 1 in C ; :: thesis: ( not A in B or 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;
A2: S₁[ {} ] ;
A3: for B being Ordinal st S₁[B] holds
S₁[ succ B]

proof

let B be Ordinal; :: thesis: ( S₁[B] implies S₁[ succ B] )
assume A4: 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 A5: A c= B by ORDINAL1:34;
A6: exp C,B in exp C,(succ B) by A1, Th23;

now

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

end;

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

end;

A7: 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

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
A8: ( B <> {} & B is limit_ordinal ) and
A9: for D being Ordinal st D in B holds
S₁[D] ; :: thesis: S₁[B]
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
deffunc H₁( Ordinal) -> set = exp C,$1;
consider fi being Ordinal-Sequence such that
A11: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
A12: exp C,B = lim fi by A8, A11, ORDINAL2:62;
fi is increasing

proof

let B1, B2 be Ordinal; :: according to ORDINAL2:def 16 :: thesis: ( not B1 in B2 or not B2 in dom fi or fi . B1 in fi . B2 )
assume A13: ( B1 in B2 & B2 in dom fi ) ; :: thesis: fi . B1 in fi . B2
then ( B1 in dom fi & S₁[B2] ) by A9, A11, ORDINAL1:19;
then ( fi . B1 = exp C,B1 & fi . B2 = exp C,B2 & exp C,B1 in exp C,B2 ) by A11, A13;
hence fi . B1 in fi . B2 ; :: thesis: verum

end;

then A14: sup fi = lim fi by A8, A11, Th8;
fi . A = exp C,A by A10, A11;
then ( exp C,A in rng fi & sup fi = sup (rng fi) ) by A10, A11, FUNCT_1:def 5;
hence exp C,A in exp C,B by A12, A14, ORDINAL2:27; :: thesis: verum

end;

for B being Ordinal holds S₁[B] from ORDINAL2:sch 1(A2, A3, A7);
hence ( not A in B or exp C,A in exp C,B ) ; :: thesis: verum