let W be Universe; :: thesis: for L being DOMAIN-Sequence of W st omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L ) )

let L be DOMAIN-Sequence of W; :: thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) implies ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L ) ) )

assume ( omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) ) ; :: thesis: ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L ) )

then consider phi being Ordinal-Sequence of W such that

A1: ( phi is increasing & phi is continuous ) and

A2: for a being Ordinal of W st phi . a = a & {} <> a holds

L . a is_elementary_subsystem_of Union L by Th30;

take phi ; :: thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L ) )

thus ( phi is increasing & phi is continuous ) by A1; :: thesis: for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L

let a be Ordinal of W; :: thesis: ( phi . a = a & {} <> a implies L . a <==> Union L )

assume ( phi . a = a & {} <> a ) ; :: thesis: L . a <==> Union L

hence L . a <==> Union L by A2, Th9; :: thesis: verum

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) holds

ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L ) )

let L be DOMAIN-Sequence of W; :: thesis: ( omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) implies ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L ) ) )

assume ( omega in W & ( for a, b being Ordinal of W st a in b holds

L . a c= L . b ) & ( for a being Ordinal of W st a <> {} & a is limit_ordinal holds

L . a = Union (L | a) ) ) ; :: thesis: ex phi being Ordinal-Sequence of W st

( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L ) )

then consider phi being Ordinal-Sequence of W such that

A1: ( phi is increasing & phi is continuous ) and

A2: for a being Ordinal of W st phi . a = a & {} <> a holds

L . a is_elementary_subsystem_of Union L by Th30;

take phi ; :: thesis: ( phi is increasing & phi is continuous & ( for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L ) )

thus ( phi is increasing & phi is continuous ) by A1; :: thesis: for a being Ordinal of W st phi . a = a & {} <> a holds

L . a <==> Union L

let a be Ordinal of W; :: thesis: ( phi . a = a & {} <> a implies L . a <==> Union L )

assume ( phi . a = a & {} <> a ) ; :: thesis: L . a <==> Union L

hence L . a <==> Union L by A2, Th9; :: thesis: verum