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

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

end;

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