theorem Th45: :: MYCIELSK:45

for n being Nat
for R being NatRelStr of n
for S being Subset of (Mycielskian R) st S = n holds
R = subrelstr S