let A be limit_ordinal infinite Ordinal; :: thesis: for X, Y being Subset of A st X is stationary & X c= Y holds

Y is stationary

let X, Y be Subset of A; :: thesis: ( X is stationary & X c= Y implies Y is stationary )

assume A1: X is stationary ; :: thesis: ( not X c= Y or Y is stationary )

assume A2: X c= Y ; :: thesis: Y is stationary

let Z1 be Subset of A; :: according to CARD_LAR:def 7 :: thesis: ( Z1 is closed & Z1 is unbounded implies not Y /\ Z1 is empty )

assume ( Z1 is closed & Z1 is unbounded ) ; :: thesis: not Y /\ Z1 is empty

then not X /\ Z1 is empty by A1;

then A3: ex x being object st x in X /\ Z1 by XBOOLE_0:def 1;

X /\ Z1 c= Y /\ Z1 by A2, XBOOLE_1:26;

hence not Y /\ Z1 is empty by A3; :: thesis: verum

Y is stationary

let X, Y be Subset of A; :: thesis: ( X is stationary & X c= Y implies Y is stationary )

assume A1: X is stationary ; :: thesis: ( not X c= Y or Y is stationary )

assume A2: X c= Y ; :: thesis: Y is stationary

let Z1 be Subset of A; :: according to CARD_LAR:def 7 :: thesis: ( Z1 is closed & Z1 is unbounded implies not Y /\ Z1 is empty )

assume ( Z1 is closed & Z1 is unbounded ) ; :: thesis: not Y /\ Z1 is empty

then not X /\ Z1 is empty by A1;

then A3: ex x being object st x in X /\ Z1 by XBOOLE_0:def 1;

X /\ Z1 c= Y /\ Z1 by A2, XBOOLE_1:26;

hence not Y /\ Z1 is empty by A3; :: thesis: verum