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 )

proof

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 A2: B1 in A ; :: thesis: ex C being Ordinal st
( C in X & B1 c= C )
not X c= B1 by A1, A2, Th5;
then consider x being set such that
A3: x in X and
A4: not x in B1 by TARSKI:def 3;
reconsider x1 = x as Element of A by A3;
take x1 ; :: thesis: ( x1 in X & B1 c= x1 )
thus x1 in X by A3; :: thesis: B1 c= x1
thus B1 c= x1 by A4, ORDINAL1:26; :: thesis: verum

end;

assume A5: for B1 being Ordinal st B1 in A holds
ex C being Ordinal st
( C in X & B1 c= C ) ; :: thesis: X is unbounded
assume not X is unbounded ; :: thesis: contradiction
then consider B1 being Ordinal such that
A6: B1 in A and
A7: X c= B1 by Th5;
consider C being Ordinal such that
A8: C in X and
A9: B1 c= C by A5, A6;
X c= C by A7, A9, XBOOLE_1:1;
then C in C by A8;
hence contradiction ; :: thesis: verum