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