( (1.REAL 2) `1 = 1 & (1.REAL 2) `2 = 1 ) by Th4, EUCLID:52;