let a, b be Ordinal; :: thesis: ( not a \ b is empty & a \ b is finite implies ex n being Nat st a = b +^ n )
assume A1: ( not a \ b is empty & a \ b is finite ) ; :: thesis: ex n being Nat st a = b +^ n
set x = the Element of a \ b;
A2: ( the Element of a \ b in a & the Element of a \ b nin b ) by A1, XBOOLE_0:def 5;
then b c= the Element of a \ b by ORDINAL6:4;
then consider c being Ordinal such that
A3: ( a = b +^ c & c <> {} ) by A2, ORDINAL1:12, ORDINAL3:28;
deffunc H₁( Ordinal) -> set = b +^ $1;
consider f being Sequence such that
A4: ( dom f = omega & ( for d being Ordinal st d in omega holds
f . d = H₁(d) ) ) from ORDINAL2:sch 2();
f is one-to-one

proof

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume A5: ( x in dom f & y in dom f & f . x = f . y & x <> y ) ; :: thesis: contradiction
then reconsider x = x, y = y as Element of omega by A4;
A6: ( f . x = H₁(x) & f . y = H₁(y) ) by A4;
( x in y or y in x ) by A5, ORDINAL1:14;
then ( b +^ x in b +^ y or b +^ y in b +^ x ) by ORDINAL2:32;
hence contradiction by A5, A6; :: thesis: verum

end;

then A7: omega , rng f are_equipotent by A4;

now :: thesis: not omega c= c

assume omega c= c ; :: thesis: contradiction
then A8: H₁( omega ) c= a by A3, ORDINAL2:33;
rng f c= a \ b

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in a \ b )
assume y in rng f ; :: thesis: y in a \ b
then consider x being object such that
A9: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
reconsider x = x as Element of omega by A4, A9;
A10: y = H₁(x) by A4, A9;
( b c= H₁(x) & H₁(x) in H₁( omega ) ) by ORDINAL2:32, ORDINAL3:24;
then ( y nin b & y in a ) by A8, A10, ORDINAL6:4;
hence y in a \ b by XBOOLE_0:def 5; :: thesis: verum

end;

hence contradiction by A1, A7, CARD_1:38; :: thesis: verum

end;

then c in omega by ORDINAL6:4;
hence ex n being Nat st a = b +^ n by A3; :: thesis: verum