let x be object ; :: according to TARSKI:def 3,MARGREL1:def 16 :: 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 object such that
A2: ( y in dom (p 'eqv' q) & x = (p 'eqv' q) . y ) by FUNCT_1:def 3;
x = 'not' ((p . y) 'xor' (q . y)) by A2, Def7;
then ( x = FALSE or x = TRUE ) by XBOOLEAN:def 3;
hence x in BOOLEAN ; :: thesis: verum