let N, M be ExtNat; :: thesis: ( N <= M implies ex K being ExtNat st M = N + K )
assume A1: N <= M ; :: thesis: ex K being ExtNat st M = N + K

per cases ( M is Nat or M = +infty ) by Th3;

suppose M is Nat ; :: thesis: ex K being ExtNat st M = N + K

then reconsider m = M as Nat ;
m in NAT by ORDINAL1:def 12;
then N in NAT by A1, Th5;
then reconsider n = N as Nat ;
consider k being Nat such that
A2: m = n + k by A1, NAT_1:10;
reconsider K = k as ExtNat ;
take K ; :: thesis: M = N + K
m = n + k by A2;
hence M = N + K ; :: thesis: verum

end;

suppose A3: M = +infty ; :: thesis: ex K being ExtNat st M = N + K

take M ; :: thesis: M = N + M
thus M = N + M by A3, XXREAL_3:def 2; :: thesis: verum

end;

end;