theorem :: STRUCT_0:2

for F being non degenerated ZeroOneStr holds 1. F in NonZero F