let A be Ordinal; :: thesis: ( A is finite implies Day A is finite )
assume A1: A is finite ; :: thesis: Day A is finite
defpred S₁[ Nat] means Day $1 is finite ;
A2: S₁[ 0 ] by SURREAL0:2;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
set n1 = n + 1;
Day (n + 1) c= [:(bool (Day n)),(bool (Day n)):]

proof

let o1, o2 be object ; :: according to RELAT_1:def 3 :: thesis: ( not [o1,o2] in Day (n + 1) or [o1,o2] in [:(bool (Day n)),(bool (Day n)):] )
assume A5: [o1,o2] in Day (n + 1) ; :: thesis: [o1,o2] in [:(bool (Day n)),(bool (Day n)):]
reconsider o1 = o1, o2 = o2 as set by TARSKI:1;
A6: ( o1 c= o1 \/ o2 & o2 c= o1 \/ o2 ) by XBOOLE_1:7;
o1 \/ o2 c= Day n

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in o1 \/ o2 or a in Day n )
assume a in o1 \/ o2 ; :: thesis: a in Day n
then consider O being Ordinal such that
A7: ( O in n + 1 & a in Day O ) by A5, SURREAL0:46;
A8: O in Segm (n + 1) by A7;
then reconsider O = O as Nat ;
O < n + 1 by A8, NAT_1:44;
then O <= n by NAT_1:13;
then Segm O c= Segm n by NAT_1:39;
then Day O c= Day n by SURREAL0:35;
hence a in Day n by A7; :: thesis: verum

end;

then ( o1 c= Day n & o2 c= Day n ) by A6, XBOOLE_1:1;
hence [o1,o2] in [:(bool (Day n)),(bool (Day n)):] by ZFMISC_1:87; :: thesis: verum

end;

hence S₁[n + 1] by A4; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence Day A is finite by A1; :: thesis: verum