let g be Element of C -States X; :: thesis: ( g is Function-yielding & g is the carrier of B -defined )
( C -States X is empty or not C -States X is empty ) ;
then ( g is empty or g in C -States X ) by SUBSET_1:def 1;
hence ( g is Function-yielding & g is the carrier of B -defined ) by Th43, RELAT_1:171; :: thesis: verum