for s, q being Nat st s <= q holds
(GoCross_Partial_Union (pm,k)) . s c= (GoCross_Partial_Union (pm,k)) . q

proof

let s, q be Nat; :: thesis: ( s <= q implies (GoCross_Partial_Union (pm,k)) . s c= (GoCross_Partial_Union (pm,k)) . q )
assume A1: s <= q ; :: thesis: (GoCross_Partial_Union (pm,k)) . s c= (GoCross_Partial_Union (pm,k)) . q
consider j being Nat such that
S2: q = s + j by A1, NAT_1:10;
defpred S₁[ Nat] means (GoCross_Partial_Union (pm,k)) . s c= (GoCross_Partial_Union (pm,k)) . (s + k);
J1: S₁[ 0 ] ;
J2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume B1: S₁[n] ; :: thesis: S₁[n + 1]
B20: (GoCross_Partial_Union (pm,k)) . ((s + n) + 1) = ((GoCross_Partial_Union (pm,k)) . (s + n)) \/ ((GoCross_Seq_REAL (pm,k)) . ((s + n) + 1)) by Def5;
(GoCross_Partial_Union (pm,k)) . s c= (GoCross_Partial_Union (pm,k)) . (s + (n + 1)) by B1, XBOOLE_0:def 3, B20;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(J1, J2);
hence (GoCross_Partial_Union (pm,k)) . s c= (GoCross_Partial_Union (pm,k)) . q by S2; :: thesis: verum

end;

hence GoCross_Partial_Union (pm,k) is non-descending ; :: thesis: verum