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