set U = Polish-expression-set (L,E);
consider a, b being object such that
A1: a in L and
A2: b in L and
A3: a <> b by ZFMISC_1:def 10;
reconsider t = a, u = b as Element of L by A1, A2;
reconsider m = E . t, n = E . u as Nat ;
reconsider v = (Polish-operation (L,E,m,t)) . the Element of (Polish-expression-set (L,E)) ^^ m as Polish-WFF of L,E by Th39;
reconsider w = (Polish-operation (L,E,n,u)) . the Element of (Polish-expression-set (L,E)) ^^ n as Polish-WFF of L,E by Th39;
( Polish-WFF-head v = t & Polish-WFF-head w = u ) ;
hence not Polish-expression-set (L,E) is trivial by A3, ZFMISC_1:def 10; :: thesis: verum