theorem Th37: :: MYCIELSK:37

for n being Nat
for R being NatRelStr of n holds the carrier of R c= the carrier of (Mycielskian R)