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

( 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