let fi be Ordinal-Sequence; :: thesis: ( dom fi <> {} & dom fi is limit_ordinal & fi is increasing implies ( sup fi is_limes_of fi & lim fi = sup fi ) )

assume that

A1: ( dom fi <> {} & dom fi is limit_ordinal ) and

A2: for A, B being Ordinal st A in B & B in dom fi holds

fi . A in fi . B ; :: according to ORDINAL2:def 12 :: thesis: ( sup fi is_limes_of fi & lim fi = sup fi )

reconsider x = fi . {} as Ordinal ;

{} in dom fi by A1, ORDINAL3:8;

then A3: x in rng fi by FUNCT_1:def 3;

thus sup fi is_limes_of fi :: thesis: lim fi = sup fi

assume that

A1: ( dom fi <> {} & dom fi is limit_ordinal ) and

A2: for A, B being Ordinal st A in B & B in dom fi holds

fi . A in fi . B ; :: according to ORDINAL2:def 12 :: thesis: ( sup fi is_limes_of fi & lim fi = sup fi )

reconsider x = fi . {} as Ordinal ;

{} in dom fi by A1, ORDINAL3:8;

then A3: x in rng fi by FUNCT_1:def 3;

thus sup fi is_limes_of fi :: thesis: lim fi = sup fi

proof
end;

hence
lim fi = sup fi
by ORDINAL2:def 10; :: thesis: verumper cases
( sup fi = 0 or sup fi <> 0 )
;

:: according to ORDINAL2:def 9end;

:: according to ORDINAL2:def 9

case
sup fi = 0
; :: thesis: ex b_{1} being set st

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or fi . b_{2} = 0 ) ) )

( b

( not b

hence
ex b_{1} being set st

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or fi . b_{2} = 0 ) ) )
by A3, ORDINAL2:19; :: thesis: verum

end;( b

( not b

case
sup fi <> 0
; :: thesis: for b_{1}, b_{2} being set holds

( not b_{1} in sup fi or not sup fi in b_{2} or ex b_{3} being set st

( b_{3} in dom fi & ( for b_{4} being set holds

( not b_{3} c= b_{4} or not b_{4} in dom fi or ( b_{1} in fi . b_{4} & fi . b_{4} in b_{2} ) ) ) ) )

( not b

( b

( not b

let A, B be Ordinal; :: thesis: ( not A in sup fi or not sup fi in B or ex b_{1} being set st

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or ( A in fi . b_{2} & fi . b_{2} in B ) ) ) ) )

assume that

A4: A in sup fi and

A5: sup fi in B ; :: thesis: ex b_{1} being set st

( b_{1} in dom fi & ( for b_{2} being set holds

( not b_{1} c= b_{2} or not b_{2} in dom fi or ( A in fi . b_{2} & fi . b_{2} in B ) ) ) )

consider C being Ordinal such that

A6: C in rng fi and

A7: A c= C by A4, ORDINAL2:21;

consider x being object such that

A8: x in dom fi and

A9: C = fi . x by A6, FUNCT_1:def 3;

reconsider x = x as Ordinal by A8;

take M = succ x; :: thesis: ( M in dom fi & ( for b_{1} being set holds

( not M c= b_{1} or not b_{1} in dom fi or ( A in fi . b_{1} & fi . b_{1} in B ) ) ) )

thus M in dom fi by A1, A8, ORDINAL1:28; :: thesis: for b_{1} being set holds

( not M c= b_{1} or not b_{1} in dom fi or ( A in fi . b_{1} & fi . b_{1} in B ) )

let D be Ordinal; :: thesis: ( not M c= D or not D in dom fi or ( A in fi . D & fi . D in B ) )

assume that

A10: M c= D and

A11: D in dom fi ; :: thesis: ( A in fi . D & fi . D in B )

reconsider E = fi . D as Ordinal ;

x in M by ORDINAL1:6;

then C in E by A2, A9, A10, A11;

hence A in fi . D by A7, ORDINAL1:12; :: thesis: fi . D in B

fi . D in rng fi by A11, FUNCT_1:def 3;

then E in sup fi by ORDINAL2:19;

hence fi . D in B by A5, ORDINAL1:10; :: thesis: verum

end;( b

( not b

assume that

A4: A in sup fi and

A5: sup fi in B ; :: thesis: ex b

( b

( not b

consider C being Ordinal such that

A6: C in rng fi and

A7: A c= C by A4, ORDINAL2:21;

consider x being object such that

A8: x in dom fi and

A9: C = fi . x by A6, FUNCT_1:def 3;

reconsider x = x as Ordinal by A8;

take M = succ x; :: thesis: ( M in dom fi & ( for b

( not M c= b

thus M in dom fi by A1, A8, ORDINAL1:28; :: thesis: for b

( not M c= b

let D be Ordinal; :: thesis: ( not M c= D or not D in dom fi or ( A in fi . D & fi . D in B ) )

assume that

A10: M c= D and

A11: D in dom fi ; :: thesis: ( A in fi . D & fi . D in B )

reconsider E = fi . D as Ordinal ;

x in M by ORDINAL1:6;

then C in E by A2, A9, A10, A11;

hence A in fi . D by A7, ORDINAL1:12; :: thesis: fi . D in B

fi . D in rng fi by A11, FUNCT_1:def 3;

then E in sup fi by ORDINAL2:19;

hence fi . D in B by A5, ORDINAL1:10; :: thesis: verum