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

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