let B be Polish-arity-function; :: thesis: for J being Polish-ext-set of B st ( {} in J or {} in dom B ) holds
( J = {{}} & Polish-WFF-set B = {{}} & dom B = {{}} & Polish-ext-complement (B,J) = {} )
let J be Polish-ext-set of B; :: thesis: ( ( {} in J or {} in dom B ) implies ( J = {{}} & Polish-WFF-set B = {{}} & dom B = {{}} & Polish-ext-complement (B,J) = {} ) )
set T = dom B;
reconsider A = B as Polish-arity-function of dom B by Th1;
set V = Polish-WFF-set B;
assume A1: ( {} in J or {} in dom B ) ; :: thesis: ( J = {{}} & Polish-WFF-set B = {{}} & dom B = {{}} & Polish-ext-complement (B,J) = {} )
( {} in dom B implies {} in J )

proof

assume B2: {} in dom B ; :: thesis: {} in J
then dom B = {{}} by POLNOT_1:46;
then A . {} = 0 by B2, Lm5;
then B3: {} in Polish-atoms ((dom B),A) by B2, POLNOT_1:def 7;
Polish-atoms ((dom B),A) c= J by POLNOT_1:34;
hence {} in J by B3; :: thesis: verum

end;

hence A3: J = {{}} by A1, POLNOT_1:46; :: thesis: ( Polish-WFF-set B = {{}} & dom B = {{}} & Polish-ext-complement (B,J) = {} )
then Polish-WFF-set B is non empty trivial Subset of J by Th8;
hence A4: Polish-WFF-set B = {{}} by A3, Lm22; :: thesis: ( dom B = {{}} & Polish-ext-complement (B,J) = {} )
Polish-WFF-set B = Polish-expression-set ((dom B),A) by Def4;
then Polish-atoms ((dom B),A) is non empty trivial Subset of (Polish-WFF-set B) by A4, POLNOT_1:36;
then Polish-atoms ((dom B),A) = {{}} by A4, Lm22;
then {} in Polish-atoms ((dom B),A) by TARSKI:def 1;
then {} in dom B by POLNOT_1:def 7;
hence A5: dom B = {{}} by POLNOT_1:46; :: thesis: Polish-ext-complement (B,J) = {}
for a being object holds not a in Polish-ext-complement (B,J) by A3, A5, Lm21;
hence Polish-ext-complement (B,J) = {} by XBOOLE_0:def 1; :: thesis: verum