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

proof

let s, q be Nat; :: thesis: ( s <= q implies (GoCross_Union pm) . s c= (GoCross_Union pm) . q )
assume s <= q ; :: thesis: (GoCross_Union pm) . s c= (GoCross_Union pm) . q
then consider j being Nat such that
S2: q = s + j by NAT_1:10;
defpred S₁[ Nat] means (GoCross_Union pm) . s c= (GoCross_Union pm) . (s + pm);
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_Union pm) . ((s + n) + 1) = ((GoCross_Union pm) . (s + n)) \/ (Union (GoCross_Partial_Union (pm,((s + n) + 1)))) by Def6;
(GoCross_Union pm) . (s + n) c= (GoCross_Union pm) . (s + (n + 1)) by XBOOLE_0:def 3, B20;
hence S₁[n + 1] by B1, XBOOLE_1:1; :: thesis: verum

end;

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

end;

hence GoCross_Union pm is non-descending ; :: thesis: verum