let x be set ; :: according to TARSKI:def 3,MARGREL1:def 17 :: thesis: ( not x in rng (p 'eqv' q) or x in BOOLEAN )
assume x in rng (p 'eqv' q) ; :: thesis: x in BOOLEAN
then consider y being set such that
A3: y in dom (p 'eqv' q) and
A4: x = (p 'eqv' q) . y by FUNCT_1:def 5;
x = 'not' ((p . y) 'xor' (q . y)) by A3, A4, Def10;
then ( x = FALSE or x = TRUE ) by XBOOLEAN:def 3;
hence x in BOOLEAN ; :: thesis: verum