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 H1( 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 = H1(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 = H1(x) & f . y = H1(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: H1( 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 = H1(x) by A4, A9;
( b c= H1(x) & H1(x) in H1( 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