set f = Euler_factorization_2 n;
let e1, e2 be ExtReal; :: according to VALUED_0:def 13 :: thesis: ( not e1 in proj1 (Euler_factorization_2 n) or not e2 in proj1 (Euler_factorization_2 n) or e2 <= e1 or not (Euler_factorization_2 n) . e2 <= (Euler_factorization_2 n) . e1 )
assume A1: ( e1 in dom (Euler_factorization_2 n) & e2 in dom (Euler_factorization_2 n) ) ; :: thesis: ( e2 <= e1 or not (Euler_factorization_2 n) . e2 <= (Euler_factorization_2 n) . e1 )
reconsider p1 = e1, p2 = e2 as Prime by A1, Th29;
( (Euler_factorization_2 n) . p1 = p1 - 1 & (Euler_factorization_2 n) . p2 = p2 - 1 ) by A1, Def3;
hence ( e2 <= e1 or not (Euler_factorization_2 n) . e2 <= (Euler_factorization_2 n) . e1 ) by XREAL_1:8; :: thesis: verum