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;