let L be ZeroOneStr ; :: thesis: ( not L is degenerated implies not L is trivial )
assume A1: not L is degenerated ; :: thesis: not L is trivial
assume L is trivial ; :: thesis: contradiction
then 0. L = 1. L by Def10;
hence contradiction by A1, Def8; :: thesis: verum