hereby :: thesis: ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies (non_op C) term a is expression of C, an_Adj C )

given a9 being expression of C, an_Adj C such that A1: a = (non_op C) term a9 ; :: thesis: a | <*0 *> is expression of C, an_Adj C
A2: a = [non_op ,the carrier of C] -tree <*a9*> by A1, Th43;
len <*a9*> = 1 by FINSEQ_1:57;
then a | <*0 *> = <*a9*> . (0 + 1) by A2, TREES_4:def 4;
hence a | <*0 *> is expression of C, an_Adj C by FINSEQ_1:57; :: thesis: verum

end;

thus ( ( for a9 being expression of C, an_Adj C holds not a = (non_op C) term a9 ) implies (non_op C) term a is expression of C, an_Adj C ) by Th43; :: thesis: verum