reconsider b = bool X as Subset-Family of X ;
set F = { x where x is Subset-Family of X : x is Coherence_Space } ;
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