let A be limit_ordinal infinite Ordinal; :: thesis: for B1 being Ordinal
for X being Subset of A st X is unbounded & B1 in A holds
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
let B1 be Ordinal; :: thesis: for X being Subset of A st X is unbounded & B1 in A holds
ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
let X be Subset of A; :: thesis: ( X is unbounded & B1 in A implies ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } )
assume A1: X is unbounded ; :: thesis: ( not B1 in A or ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } )
assume B1 in A ; :: thesis: ex B3 being Element of A st B3 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
then succ B1 in A by ORDINAL1:28;
then consider B3 being Ordinal such that
A2: B3 in X and
A3: succ B1 c= B3 by A1, Th6;
reconsider B4 = B3 as Element of A by A2;
take B4 ; :: thesis: B4 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) }
B1 in B3 by A3, ORDINAL1:21;
hence B4 in { B2 where B2 is Element of A : ( B2 in X & B1 in B2 ) } by A2; :: thesis: verum