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 ) )
reconsider Y = X /\ B as Subset of B by XBOOLE_1:17;
assume not sup (X /\ B) = B ; :: thesis: ex B1 being Ordinal st
( B1 in B & X /\ B c= B1 )
then Y is bounded ;
then consider B1 being Ordinal such that
A1: ( B1 in B & Y c= B1 ) by Th4;
take B1 ; :: thesis: ( B1 in B & X /\ B c= B1 )
thus ( B1 in B & X /\ B c= B1 ) by A1; :: thesis: verum