theorem Th42: :: EUCLID_8:50

for p being Element of REAL 3 holds
( len p = 3 & dom p = Seg 3 )