the carrier of Trivial-doubleLoopStr = {0} by CARD_1:49;
hence the carrier of Trivial-doubleLoopStr is 1 -element ; :: according to STRUCT_0:def 19 :: thesis: Trivial-doubleLoopStr is strict
thus Trivial-doubleLoopStr is strict ; :: thesis: verum