take ZeroStr(# 1,(In (0,1)) #) ; :: thesis: ( ZeroStr(# 1,(In (0,1)) #) is trivial & not ZeroStr(# 1,(In (0,1)) #) is empty )
thus ( ZeroStr(# 1,(In (0,1)) #) is trivial & not ZeroStr(# 1,(In (0,1)) #) is empty ) by CARD_1:49; :: thesis: verum