take S = ZeroStr(# 2,(In 0 ,2) #); :: thesis: ( S is strict & not S is trivial )
( 0 in 2 & 1 in 2 ) by CARD_1:88, TARSKI:def 2;
hence ( S is strict & not S is trivial ) by Def10; :: thesis: verum