let B be Polish-arity-function; :: thesis: for J being Polish-ext-set of B
for a being object st a in Polish-ext-complement (B,J) holds
( a in J & a in Polish-ext-domain (B,J) & not a in dom B )
let J be Polish-ext-set of B; :: thesis: for a being object st a in Polish-ext-complement (B,J) holds
( a in J & a in Polish-ext-domain (B,J) & not a in dom B )
let a be object ; :: thesis: ( a in Polish-ext-complement (B,J) implies ( a in J & a in Polish-ext-domain (B,J) & not a in dom B ) )
set T = dom B;
assume A2: a in Polish-ext-complement (B,J) ; :: thesis: ( a in J & a in Polish-ext-domain (B,J) & not a in dom B )
then consider p being Element of J such that
A3: a = p and
A4: not p is dom B -headed ;
thus a in J by A3; :: thesis: ( a in Polish-ext-domain (B,J) & not a in dom B )
thus a in Polish-ext-domain (B,J) by A2, XBOOLE_0:def 3; :: thesis: not a in dom B
A6: dom B is dom B -headed by POLNOT_1:50;
assume a in dom B ; :: thesis: contradiction
hence contradiction by A3, A4, A6; :: thesis: verum