:: deftheorem defines 1. STRUCT_0:def 7 :
for S being OneStr holds 1. S = the OneF of S;