consider x being object such that
A1: x in F by XBOOLE_0:def 1;
reconsider x1 = x as PNPair by A1;
x1 ^ in F ^ by A1;
hence not F ^ is empty ; :: thesis: verum