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

X is unbounded

let X be Subset of A; :: thesis: ( X is stationary implies X is unbounded )

assume A1: X is stationary ; :: thesis: X is unbounded

assume X is bounded ; :: thesis: contradiction

then consider B1 being Ordinal such that

A2: B1 in A and

A3: X c= B1 by Th4;

A \ B1 misses B1 by XBOOLE_1:79;

then A \ B1 misses X by A3, XBOOLE_1:63;

then A4: (A \ B1) /\ X = {} by XBOOLE_0:def 7;

( A \ B1 is closed & A \ B1 is unbounded ) by A2, Th12;

hence contradiction by A1, A4; :: thesis: verum

X is unbounded

let X be Subset of A; :: thesis: ( X is stationary implies X is unbounded )

assume A1: X is stationary ; :: thesis: X is unbounded

assume X is bounded ; :: thesis: contradiction

then consider B1 being Ordinal such that

A2: B1 in A and

A3: X c= B1 by Th4;

A \ B1 misses B1 by XBOOLE_1:79;

then A \ B1 misses X by A3, XBOOLE_1:63;

then A4: (A \ B1) /\ X = {} by XBOOLE_0:def 7;

( A \ B1 is closed & A \ B1 is unbounded ) by A2, Th12;

hence contradiction by A1, A4; :: thesis: verum