set g = f | X;
let e1, e2 be ExtReal; :: according to VALUED_0:def 15 :: thesis: ( e1 in dom (f | X) & e2 in dom (f | X) & e1 <= e2 implies (f | X) . e1 <= (f | X) . e2 )
assume A1: ( e1 in dom (f | X) & e2 in dom (f | X) ) ; :: thesis: ( not e1 <= e2 or (f | X) . e1 <= (f | X) . e2 )
A2: dom (f | X) c= dom f by RELAT_1:60;
( f . e1 = (f | X) . e1 & f . e2 = (f | X) . e2 ) by A1, FUNCT_1:47;
hence ( not e1 <= e2 or (f | X) . e1 <= (f | X) . e2 ) by A1, A2, Def11; :: thesis: verum