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

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