set U = Polish-WFF-set (T,A);
(Polish-WFF-set (T,A)) ^^ 1 = Polish-WFF-set (T,A) by Th8;
hence Polish-operation (T,A,t) is UnOp of (Polish-WFF-set (T,A)) by A1; :: thesis: verum