( not a <= 1 or a = 1 or a < 1 ) by XXREAL_0:1;
hence ( a is trivial iff a <= 1 ) by NAT_2:def 1, NAT_1:14; :: thesis: verum