let x be object ; :: according to TARSKI:def 3,MARGREL1:def 16 :: thesis: ( not x in rng (p 'xor' q) or x in BOOLEAN )
assume x in rng (p 'xor' q) ; :: thesis: x in BOOLEAN
then consider y being object such that
A1: ( y in dom (p 'xor' q) & x = (p 'xor' q) . y ) by FUNCT_1:def 3;
x = (p . y) 'xor' (q . y) by A1, Def3;
then ( x = FALSE or x = TRUE ) by XBOOLEAN:def 3;
hence x in BOOLEAN ; :: thesis: verum