let L be non trivial Polish-language; :: thesis: for E being Polish-arity-function of L
for F being Polish-WFF of L,E holds
( F in Polish-atoms (L,E) iff Polish-arity F = 0 )
let E be Polish-arity-function of L; :: thesis: for F being Polish-WFF of L,E holds
( F in Polish-atoms (L,E) iff Polish-arity F = 0 )
let F be Polish-WFF of L,E; :: thesis: ( F in Polish-atoms (L,E) iff Polish-arity F = 0 )
thus ( F in Polish-atoms (L,E) implies Polish-arity F = 0 ) :: thesis: ( Polish-arity F = 0 implies F in Polish-atoms (L,E) )

proof

assume A1: F in Polish-atoms (L,E) ; :: thesis: Polish-arity F = 0
then F in L by Def7;
then Polish-WFF-head F = F by Th53;
hence Polish-arity F = 0 by A1, Def7; :: thesis: verum

end;

assume A10: Polish-arity F = 0 ; :: thesis: F in Polish-atoms (L,E)
then L -tail F in (Polish-WFF-set (L,E)) ^^ 0 by Th67;
then L -tail F in {{}} by Th6;
then L -tail F = {} by TARSKI:def 1;
then F = (L -head F) ^ {} ;
then F = Polish-WFF-head F by FINSEQ_1:34;
hence F in Polish-atoms (L,E) by A10, Def7; :: thesis: verum