let a, b be Ordinal; :: thesis:
assume A1: a \ b <> {} ; :: thesis:
set x = the Element of a \ b;
A2: the Element of a \ b in a \ b by A1;
A3: ( the Element of a \ b in a & the Element of a \ b nin b ) by A1, XBOOLE_0:def 5;
then A: b c= the Element of a \ b by ORDINAL6:4;
not b in b ;
then ( b in a & b nin b ) by A, A3, ORDINAL1:12;
then A4: b in a \ b by XBOOLE_0:def 5;
hence inf (a \ b) c= b by ORDINAL2:14; :: according to XBOOLE_0:def 10 :: thesis:
inf (a \ b) in a \ b by A2, ORDINAL2:17;
then inf (a \ b) nin b by XBOOLE_0:def 5;
hence b c= inf (a \ b) by ORDINAL6:4; :: thesis:
A5: On (a \ b) = a \ b by ORDINAL6:2;
thus sup (a \ b) c= a by A5, ORDINAL2:def 3; :: according to XBOOLE_0:def 10 :: thesis:
thus a c= sup (a \ b) :: thesis:

let c be Ordinal; :: according to ORDINAL1:def 5 :: thesis:
assume A6: c in a ; :: thesis:
A7: b in sup (a \ b) by A4, ORDINAL2:19;

suppose c in b ; :: thesis:

hence c in sup (a \ b) by A7, ORDINAL1:10; :: thesis:

end;

suppose c nin b ; :: thesis:

then c in a \ b by A6, XBOOLE_0:def 5;
hence c in sup (a \ b) by ORDINAL2:19; :: thesis:

end;

end;

end;

thus union (a \ b) c= union a by ZFMISC_1:77; :: according to XBOOLE_0:def 10 :: thesis:
for y being object st y in union a holds
y in union (a \ b)

let y be object ; :: thesis:
assume y in union a ; :: thesis:
then consider x being set such that
A8: ( y in x & x in a ) by TARSKI:def 4;
reconsider x = x as Ordinal by A8;

per cases by ORDINAL6:4;

suppose x in b ; :: thesis:

then y in b by A8, ORDINAL1:10;
hence y in union (a \ b) by A4, TARSKI:def 4; :: thesis:

end;

suppose b c= x ; :: thesis:

then x in a \ b by A8, ORDINAL6:5;
hence y in union (a \ b) by A8, TARSKI:def 4; :: thesis:

end;

end;

end;

hence union a c= union (a \ b) ; :: thesis: