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

( 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