let a, b be Ordinal; :: thesis: ( a \ b <> {} implies ( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a ) )
assume A1: a \ b <> {} ; :: thesis: ( inf (a \ b) = b & sup (a \ b) = a & union (a \ b) = union a )
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: ( b c= inf (a \ b) & sup (a \ b) = a & union (a \ b) = union a )
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: ( sup (a \ b) = a & union (a \ b) = union a )
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: ( a c= sup (a \ b) & union (a \ b) = union a )
thus a c= sup (a \ b) :: thesis: union (a \ b) = union a

proof

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

per cases ( c in b or c nin b ) ;

suppose c in b ; :: thesis: c in sup (a \ b)

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

end;

suppose c nin b ; :: thesis: c in sup (a \ b)

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

end;

end;

end;

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

proof

let y be object ; :: thesis: ( y in union a implies y in union (a \ b) )
assume y in union a ; :: thesis: y in union (a \ b)
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 ( x in b or b c= x ) by ORDINAL6:4;

suppose x in b ; :: thesis: y in union (a \ b)

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

end;

suppose b c= x ; :: thesis: y in union (a \ b)

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

end;

end;

end;

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