set FV = { [[T,TT],f] where T, TT is Element of CSp X, f is Element of FuncsC X : ( ( union TT = {} implies union T = {} ) & f is Function of (union T),(union TT) & ( for x, y being set st {x,y} in T holds
{(f . x),(f . y)} in TT ) ) } ;

now :: thesis: ex m being object st m in { [[T,TT],f] where T, TT is Element of CSp X, f is Element of FuncsC X : ( ( union TT = {} implies union T = {} ) & f is Function of (union T),(union TT) & ( for x, y being set st {x,y} in T holds
{(f . x),(f . y)} in TT ) ) }

reconsider A = bool X as Subset-Family of X ;
A is Coherence_Space by Th2;
then A in { xx where xx is Subset-Family of X : xx is Coherence_Space } ;
then reconsider A = A as Element of CSp X ;
set f = id (union A);
take m = [[A,A],(id (union A))]; :: thesis: m in { [[T,TT],f] where T, TT is Element of CSp X, f is Element of FuncsC X : ( ( union TT = {} implies union T = {} ) & f is Function of (union T),(union TT) & ( for x, y being set st {x,y} in T holds
{(f . x),(f . y)} in TT ) ) }
A1: ( union A = {} implies union A = {} ) ;
reconsider f = id (union A) as Element of FuncsC X by Th17;

now :: thesis: for x, y being set st {x,y} in A holds
{(f . x),(f . y)} in A

let x, y be set ; :: thesis: ( {x,y} in A implies {(f . x),(f . y)} in A )
assume A2: {x,y} in A ; :: thesis: {(f . x),(f . y)} in A
then x in union A by Th16;
then A3: f . x = x by FUNCT_1:18;
y in union A by A2, Th16;
hence {(f . x),(f . y)} in A by A2, A3, FUNCT_1:18; :: thesis: verum

end;

hence m in { [[T,TT],f] where T, TT is Element of CSp X, f is Element of FuncsC X : ( ( union TT = {} implies union T = {} ) & f is Function of (union T),(union TT) & ( for x, y being set st {x,y} in T holds
{(f . x),(f . y)} in TT ) ) } by A1; :: thesis: verum

end;

hence not MapsC X is empty ; :: thesis: verum