( (0. (TOP-REAL 2)) `1 = 0 & (0. (TOP-REAL 2)) `2 = 0 ) by EUCLID:52, EUCLID:54;