theorem Th10: :: CARDFIL4:11

for m, n being Nat holds [:(NAT \ (Segm m)),(NAT \ (Segm n)):] c= [:NAT,NAT:] \ [:(Segm m),(Segm n):]