let A be limit_ordinal infinite Ordinal; :: thesis: for X, Y being set st X is_stationary_in A & X c= Y & Y c= A holds
Y is_stationary_in A
let X, Y be set ; :: thesis: ( X is_stationary_in A & X c= Y & Y c= A implies Y is_stationary_in A )
assume A1: X is_stationary_in A ; :: thesis: ( not X c= Y or not Y c= A or Y is_stationary_in A )
then reconsider X1 = X as Subset of A ;
assume A2: X c= Y ; :: thesis: ( not Y c= A or Y is_stationary_in A )
assume Y c= A ; :: thesis: Y is_stationary_in A
then reconsider Y1 = Y as Subset of A ;
for Z being Subset of A st Z is closed & Z is unbounded holds
not X /\ Z is empty by A1;
then X1 is stationary ;
then Y1 is stationary by A2, Th13;
then for Z being Subset of A st Z is closed & Z is unbounded holds
not Y1 /\ Z is empty ;
hence Y is_stationary_in A ; :: thesis: verum