theorem Th2: :: EUCLID12:2

for a being Real st |.a.| = |.(1 - a).| holds
a = 1 / 2