take F = Z/ 3; :: thesis: not F is almost_trivial
A2: Z/ 3 = doubleLoopStr(# (Segm 3),(addint 3),(multint 3),(In (1,(Segm 3))),(In (0,(Segm 3))) #) by INT_3:def 12;
then reconsider t = 2 as Element of [#] F by NAT_1:44;
A3: t <> 0. F by A2, NAT_1:44, SUBSET_1:def 8;
t <> 1. F by A2, NAT_1:44, SUBSET_1:def 8;
hence not F is almost_trivial by A3; :: thesis: verum