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 a' being expression of C, an_Adj C holds
( not a' is positive or not a = (non_op C) term a' ) by A1, Def37; :: according to ABCMIZ_1:def 38 :: thesis: verum