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

proof

let x be set ; :: according to FUNCT_1:def 4 :: thesis: for b₁ being set holds
( not x in proj1 f or not b₁ in proj1 f or not f . x = f . b₁ or x = b₁ )
let y be set ; :: thesis: ( not x in proj1 f or not y in proj1 f or not f . x = f . y or x = y )
assume B1: ( 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 F0;
B2: ( f . x = H₁(x) & f . y = H₁(y) ) by F0;
( x in y or y in x ) by B1, ORDINAL1:14;
then ( b +^ x in b +^ y or b +^ y in b +^ x ) by ORDINAL2:32;
hence contradiction by B1, B2; :: thesis: verum

end;

then F2: omega , rng f are_equipotent by F0, WELLORD2:def 4;

now

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

proof

let y be set ; :: 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 set such that
A3: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
reconsider x = x as Element of omega by F0, A3;
A4: y = H₁(x) by F0, A3;
( b c= H₁(x) & H₁(x) in H₁( omega ) ) by ORDINAL2:32, ORDINAL3:24;
then ( y nin b & y in a ) by A2, A4, ORDINAL6:4;
hence y in a \ b by XBOOLE_0:def 5; :: thesis: verum

end;

hence contradiction by Z0, F2, CARD_1:38; :: thesis: verum

end;

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