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 consider x being Subset-Family of X such that
A1: ( C = x & x is Coherence_Space ) ;
thus ( C is subset-closed & C is binary_complete & not C is empty ) by A1; :: thesis: verum