for a, b being Real holds |[a,b]| = (1,2) --> (a,b) by Th4;