let A be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A holds
( X is_club_in A iff ( X is closed & X is unbounded ) )
let X be Subset of A; :: thesis: ( X is_club_in A iff ( X is closed & X is unbounded ) )
thus ( X is_club_in A implies ( X is closed & X is unbounded ) ) :: thesis: ( X is closed & X is unbounded implies X is_club_in A )
proof
assume A1: X is_club_in A ; :: thesis: ( X is closed & X is unbounded )
then X is_unbounded_in A ;
then A2: sup X = A ;
X is_closed_in A by A1;
then for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X ;
hence ( X is closed & X is unbounded ) by A2; :: thesis: verum
end;
assume A3: ( X is closed & X is unbounded ) ; :: thesis: X is_club_in A
then sup X = A ;
then A4: X is_unbounded_in A ;
for B being limit_ordinal infinite Ordinal st B in A & sup (X /\ B) = B holds
B in X by A3;
then X is_closed_in A ;
hence X is_club_in A by A4; :: thesis: verum