theorem Th10: :: COUSIN:15
for n being Nat
for s1 being sequence of (Euclid n)
for s2 being sequence of (REAL-NS n) holds
( s1 is sequence of (REAL-NS n) & s2 is sequence of (Euclid n) )