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 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;
assume A4: 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 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