set F = { x where x is Subset-Family of X : x is Coherence_Space } ;
reconsider b = bool X as Subset-Family of X by ZFMISC_1:def 1;
b is Coherence_Space by Th2;
then b in { x where x is Subset-Family of X : x is Coherence_Space } ;
hence not CSp X is empty ; :: thesis: verum