let a be expression of C, an_Adj C; :: thesis: ( a is positive implies ( a is regular & not a is negative ) )
assume A1: a is positive ; :: thesis: ( a is regular & not a is negative )
hence a is regular by Def39; :: thesis: not a is negative
thus for a9 being expression of C, an_Adj C holds
( not a9 is positive or not a = (non_op C) term a9 ) by A1, Def37; :: according to ABCMIZ_1:def 38 :: thesis: verum