theorem Th3: :: MATRIX_9:3
for f being one-to-one Function st dom f = Seg 2 & rng f = Seg 2 & not f = id (Seg 2) holds
f = Rev (id (Seg 2))