let e1 be ExtReal; :: according to VALUED_0:def 13 :: thesis: for e2 being ExtReal st e1 in dom (id X) & e2 in dom (id X) & e1 < e2 holds
(id X) . e1 < (id X) . e2
let e2 be ExtReal; :: thesis: ( e1 in dom (id X) & e2 in dom (id X) & e1 < e2 implies (id X) . e1 < (id X) . e2 )
assume that
A1: e1 in dom (id X) and
A2: e2 in dom (id X) ; :: thesis: ( not e1 < e2 or (id X) . e1 < (id X) . e2 )
(id X) . e1 = e1 by A1, FUNCT_1:18;
hence ( not e1 < e2 or (id X) . e1 < (id X) . e2 ) by A2, FUNCT_1:18; :: thesis: verum