( x 'nand' y = FALSE or x 'nand' y = TRUE ) by XBOOLEAN:def 3;
hence x 'nand' y is Element of BOOLEAN ; :: thesis: verum