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