let a, b be Ordinal; for x being object st 0 in a & not b is empty & b is limit_ordinal holds
( x in exp (a,b) iff ex c being Ordinal st
( c in b & x in exp (a,c) ) )
let x be object ; ( 0 in a & not b is empty & b is limit_ordinal implies ( x in exp (a,b) iff ex c being Ordinal st
( c in b & x in exp (a,c) ) ) )
assume A1:
( 0 in a & not b is empty & b is limit_ordinal )
; ( x in exp (a,b) iff ex c being Ordinal st
( c in b & x in exp (a,c) ) )
deffunc H1( Ordinal) -> set = exp (a,$1);
consider f being Ordinal-Sequence such that
A2:
( dom f = b & ( for c being Ordinal st c in b holds
f . c = H1(c) ) )
from ORDINAL2:sch 3();
f is non-decreasing
by A1, A2, Th8;
then
Union f is_limes_of f
by A1, A2, Th6;
then A3: Union f =
lim f
by ORDINAL2:def 10
.=
exp (a,b)
by A1, A2, ORDINAL2:45
;
given c being Ordinal such that A5:
( c in b & x in exp (a,c) )
; x in exp (a,b)
f . c = H1(c)
by A2, A5;
hence
x in exp (a,b)
by A2, A3, A5, CARD_5:2; verum