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