let UN be non trivial Universe; :: thesis: COMPLEX in UN
set X = Funcs ({0,1},REAL);
set Y = { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ;
A1: ((Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } ) \/ REAL c= (Funcs ({0,1},REAL)) \/ REAL by XBOOLE_1:13;
A2: ( 0 in UN & 1 in UN ) by Th16;
UN is axiom_GU2 ;
then A3: {0,1} in UN by A2;
A4: REAL is Element of UN by Th53;
then Funcs ({0,1},REAL) in UN by A3, CLASSES2:61;
then (Funcs ({0,1},REAL)) \/ REAL in UN by A4, CLASSES2:60;
hence COMPLEX in UN by Th13, A1; :: thesis: verum