take S = ZeroOneStr(# 2,(In 0 ,2),(In 1,2) #); :: thesis: ( S is strict & not S is degenerated )
0 in 2 by CARD_1:88, TARSKI:def 2;
then ( 1 in 2 & In 0 ,2 = 0 ) by CARD_1:88, FUNCT_7:def 1, TARSKI:def 2;
then 0. S <> 1. S by FUNCT_7:def 1;
hence ( S is strict & not S is degenerated ) by Def8; :: thesis: verum