let A, B be limit_ordinal infinite Ordinal; :: thesis: for X being Subset of A st not sup (X /\ B) = B holds
ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 )
let X be Subset of A; :: thesis: ( not sup (X /\ B) = B implies ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 ) )
assume A1: not sup (X /\ B) = B ; :: thesis: ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 )
reconsider Y = X /\ B as Subset of B by XBOOLE_1:17;
not Y is unbounded by A1, Def4;
then consider B1 being Ordinal such that
A2: B1 in B and
A3: Y c= B1 by Th5;
take B1 ; :: thesis: ( B1 in B & X /\ B c= B1 )
thus ( B1 in B & X /\ B c= B1 ) by A2, A3; :: thesis: verum