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