let A be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A holds

( X is unbounded iff for B1 being Ordinal st B1 in A holds

ex C being Ordinal st

( C in X & B1 c= C ) )

let X be Subset of A; :: thesis: ( X is unbounded iff for B1 being Ordinal st B1 in A holds

ex C being Ordinal st

( C in X & B1 c= C ) )

thus ( X is unbounded implies for B1 being Ordinal st B1 in A holds

ex C being Ordinal st

( C in X & B1 c= C ) ) :: thesis: ( ( for B1 being Ordinal st B1 in A holds

ex C being Ordinal st

( C in X & B1 c= C ) ) implies X is unbounded )

ex C being Ordinal st

( C in X & B1 c= C ) ; :: thesis: X is unbounded

assume X is bounded ; :: thesis: contradiction

then consider B1 being Ordinal such that

A5: B1 in A and

A6: X c= B1 by Th4;

consider C being Ordinal such that

A7: C in X and

A8: B1 c= C by A4, A5;

X c= C by A6, A8;

then C in C by A7;

hence contradiction ; :: thesis: verum

( X is unbounded iff for B1 being Ordinal st B1 in A holds

ex C being Ordinal st

( C in X & B1 c= C ) )

let X be Subset of A; :: thesis: ( X is unbounded iff for B1 being Ordinal st B1 in A holds

ex C being Ordinal st

( C in X & B1 c= C ) )

thus ( X is unbounded implies for B1 being Ordinal st B1 in A holds

ex C being Ordinal st

( C in X & B1 c= C ) ) :: thesis: ( ( for B1 being Ordinal st B1 in A holds

ex C being Ordinal st

( C in X & B1 c= C ) ) implies X is unbounded )

proof

assume A4:
for B1 being Ordinal st B1 in A holds
assume A1:
X is unbounded
; :: thesis: for B1 being Ordinal st B1 in A holds

ex C being Ordinal st

( C in X & B1 c= C )

let B1 be Ordinal; :: thesis: ( B1 in A implies ex C being Ordinal st

( C in X & B1 c= C ) )

assume B1 in A ; :: thesis: ex C being Ordinal st

( C in X & B1 c= C )

then not X c= B1 by A1, Th4;

then consider x being object such that

A2: x in X and

A3: not x in B1 ;

reconsider x1 = x as Element of A by A2;

take x1 ; :: thesis: ( x1 in X & B1 c= x1 )

thus x1 in X by A2; :: thesis: B1 c= x1

thus B1 c= x1 by A3, ORDINAL1:16; :: thesis: verum

end;ex C being Ordinal st

( C in X & B1 c= C )

let B1 be Ordinal; :: thesis: ( B1 in A implies ex C being Ordinal st

( C in X & B1 c= C ) )

assume B1 in A ; :: thesis: ex C being Ordinal st

( C in X & B1 c= C )

then not X c= B1 by A1, Th4;

then consider x being object such that

A2: x in X and

A3: not x in B1 ;

reconsider x1 = x as Element of A by A2;

take x1 ; :: thesis: ( x1 in X & B1 c= x1 )

thus x1 in X by A2; :: thesis: B1 c= x1

thus B1 c= x1 by A3, ORDINAL1:16; :: thesis: verum

ex C being Ordinal st

( C in X & B1 c= C ) ; :: thesis: X is unbounded

assume X is bounded ; :: thesis: contradiction

then consider B1 being Ordinal such that

A5: B1 in A and

A6: X c= B1 by Th4;

consider C being Ordinal such that

A7: C in X and

A8: B1 c= C by A4, A5;

X c= C by A6, A8;

then C in C by A7;

hence contradiction ; :: thesis: verum