let A be limit_ordinal infinite Ordinal; :: thesis: for B3, B1 being Ordinal
for X being Subset of A st X /\ B3 c= B1 holds
B3 /\ (limpoints X) c= succ B1
let B3, B1 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
assume not B3 /\ (limpoints X) c= succ B1 ; :: thesis: contradiction
then consider x being set such that
A2: x in B3 /\ (limpoints X) and
A3: not x in succ B1 by TARSKI:def 3;
A4: x in B3 by A2, XBOOLE_0:def 4;
reconsider x1 = x as Element of B3 by A2, XBOOLE_0:def 4;
defpred S₁[ set ] means ( not $1 is finite & $1 is limit_ordinal & sup (X /\ $1) = $1 );
A5: x1 in { B2 where B2 is Element of A : S₁[B2] } by A2, XBOOLE_0:def 4;
succ B1 c= x1 by A3, ORDINAL1:26;
then A6: B1 in x1 by ORDINAL1:33;
A7: 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 A7, Def4;
then consider C being Ordinal such that
A8: C in Y and
A9: B1 c= C by A6, Th7;
A10: C in X by A8, XBOOLE_0:def 4;
C in B3 by A4, A8, ORDINAL1:19;
then C in X /\ B3 by A10, XBOOLE_0:def 4;
then C in B1 by A1;
then C in C by A9;
hence contradiction ; :: thesis: verum