theorem Th2: :: EUCLID_5:2

for x, y, z being Real holds
( |[x,y,z]| `1 = x & |[x,y,z]| `2 = y & |[x,y,z]| `3 = z ) ;