take S = 2-sorted(# 1,{0,1} #); :: thesis: not S is trivial'
( 0 in {0,1} & 1 in {0,1} ) by TARSKI:def 2;
hence not S is trivial' by ZFMISC_1:def 10; :: thesis: verum