theorem Th32: :: MYCIELSK:32

for n being Nat
for x, y being set st x in n & y in n holds
( [x,y] in the InternalRel of (CompleteRelStr n) iff x <> y )