set X = Polish-atoms (GRZ-symbols,GRZ-arity);
thus Polish-atoms (GRZ-symbols,GRZ-arity) c= VAR :: according to XBOOLE_0:def 10 :: thesis: VAR c= Polish-atoms (GRZ-symbols,GRZ-arity)
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Polish-atoms (GRZ-symbols,GRZ-arity) or a in VAR )
assume A11: a in Polish-atoms (GRZ-symbols,GRZ-arity) ; :: thesis: a in VAR
then GRZ-arity . a = 0 by POLNOT_1:def 7;
then A13: not a in GRZ-ops by Th4, ENUMSET1:def 1;
a in GRZ-symbols by A11, POLNOT_1:def 7;
hence a in VAR by A13, XBOOLE_0:def 3; :: thesis: verum
end;
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in VAR or a in Polish-atoms (GRZ-symbols,GRZ-arity) )
assume A2: a in VAR ; :: thesis: a in Polish-atoms (GRZ-symbols,GRZ-arity)
then A3: a in GRZ-symbols by XBOOLE_0:def 3;
not a in GRZ-ops by A2, Lm4;
then GRZ-arity . a = 0 by A3, Def4;
hence a in Polish-atoms (GRZ-symbols,GRZ-arity) by A3, POLNOT_1:def 7; :: thesis: verum