let g be Element of C -States X; :: thesis: ( g is Relation-like & g is Function-like )
( C -States X is empty or not C -States X is empty ) ;
hence ( g is Relation-like & g is Function-like ) by Th43; :: thesis: verum