theorem :: EUCLID:52

for x, y being Real holds
( |[x,y]| `1 = x & |[x,y]| `2 = y ) by FINSEQ_1:44;