let F be non degenerated ZeroOneStr ; :: thesis: 1. F in NonZero F
not 1. F in {(0. F)} by TARSKI:def 1;
hence 1. F in NonZero F by XBOOLE_0:def 5; :: thesis: verum