let A be limit_ordinal infinite Ordinal; :: thesis: for B1, B3 being Ordinal
for X being Subset of A st X /\ B3 c= B1 holds
B3 /\ (limpoints X) c= succ B1
let B1, B3 be Ordinal; :: thesis: for X being Subset of A st X /\ B3 c= B1 holds
B3 /\ (limpoints X) c= succ B1
let X be Subset of A; :: thesis: ( X /\ B3 c= B1 implies B3 /\ (limpoints X) c= succ B1 )
assume A1: X /\ B3 c= B1 ; :: thesis: B3 /\ (limpoints X) c= succ B1
defpred S₁[ set ] means ( $1 is infinite & $1 is limit_ordinal & sup (X /\ $1) = $1 );
assume not B3 /\ (limpoints X) c= succ B1 ; :: thesis: contradiction
then consider x being object such that
A2: x in B3 /\ (limpoints X) and
A3: not x in succ B1 ;
reconsider x1 = x as Element of B3 by A2, XBOOLE_0:def 4;
succ B1 c= x1 by A3, ORDINAL1:16;
then A4: B1 in x1 by ORDINAL1:21;
A5: x1 in { B2 where B2 is Element of A : S₁[B2] } by A2, XBOOLE_0:def 4;
A6: S₁[x1] from CARD_FIL:sch 1(A5);
then reconsider x2 = x1 as limit_ordinal infinite Ordinal ;
reconsider Y = X /\ x2 as Subset of x2 by XBOOLE_1:17;
Y is unbounded by A6;
then consider C being Ordinal such that
A7: C in Y and
A8: B1 c= C by A4, Th6;
A9: C in X by A7, XBOOLE_0:def 4;
x in B3 by A2, XBOOLE_0:def 4;
then C in B3 by A7, ORDINAL1:10;
then C in X /\ B3 by A9, XBOOLE_0:def 4;
then C in B1 by A1;
then C in C by A8;
hence contradiction ; :: thesis: verum