let L be non trivial Polish-language; :: thesis: for E being Polish-arity-function of L
for F being Polish-WFF of L,E st F in Polish-atoms (L,E) holds
( Polish-WFF-head F = F & L -head F = F & Polish-WFF-args F = {} )
let E be Polish-arity-function of L; :: thesis: for F being Polish-WFF of L,E st F in Polish-atoms (L,E) holds
( Polish-WFF-head F = F & L -head F = F & Polish-WFF-args F = {} )
let F be Polish-WFF of L,E; :: thesis: ( F in Polish-atoms (L,E) implies ( Polish-WFF-head F = F & L -head F = F & Polish-WFF-args F = {} ) )
assume A1: F in Polish-atoms (L,E) ; :: thesis: ( Polish-WFF-head F = F & L -head F = F & Polish-WFF-args F = {} )
then F in L by Def7;
hence ( Polish-WFF-head F = F & L -head F = F ) by Th53; :: thesis: Polish-WFF-args F = {}
then Polish-arity F = 0 by A1, Def7;
hence Polish-WFF-args F = {} by Th61; :: thesis: verum