let C be Element of CSp X; :: thesis: ( C is subset-closed & C is binary_complete & not C is empty )
C in { x where x is Subset-Family of X : x is Coherence_Space } ;
then ex x being Subset-Family of X st
( C = x & x is Coherence_Space ) ;
hence ( C is subset-closed & C is binary_complete & not C is empty ) ; :: thesis: verum