let C be initialized standardized ConstructorSignature; :: thesis: for a being quasi-adjective of C holds
( a is negative iff (a . {}) `1 = non_op )
let t be quasi-adjective of C; :: thesis: ( t is negative iff (t . {}) `1 = non_op )
per cases ( t is positive expression of C, an_Adj C or t is negative expression of C, an_Adj C ) ;
suppose A1: t is positive expression of C, an_Adj C ; :: thesis: ( t is negative iff (t . {}) `1 = non_op )
then ( (t . {}) `1 in Constructors & non_op in {*,non_op} ) by Th24, TARSKI:def 2;
hence ( t is negative iff (t . {}) `1 = non_op ) by A1, ABCMIZ_1:39, XBOOLE_0:3; :: thesis: verum
end;
suppose A2: t is negative expression of C, an_Adj C ; :: thesis: ( t is negative iff (t . {}) `1 = non_op )
then consider a being expression of C, an_Adj C such that
A3: ( a is positive & t = (non_op C) term a ) by ABCMIZ_1:def 38;
t = [non_op, the carrier of C] -tree <*a*> by A3, ABCMIZ_1:43;
then t . {} = [non_op, the carrier of C] by TREES_4:def 4;
hence ( t is negative iff (t . {}) `1 = non_op ) by A2; :: thesis: verum
end;
end;