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:40;
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:40; :: 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