theorem Th35: :: BKMODEL4:6

for u being Element of (TOP-REAL 3) holds u = |[(u . 1),(u . 2),(u . 3)]|