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

reconsider A = bool X as Subset-Family of X by ZFMISC_1:def 1;
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 = {} ) ;
then reconsider f = id (union A) as Element of FuncsC X by Th17;

now

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 & y in union A ) by Th16;
then ( f . x = x & f . y = y ) by FUNCT_1:35;
hence {(f . x),(f . y)} in A by A2; :: 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