{} is NonatomicND of V,A
by Th30;

then reconsider e = {} as TypeSCNominativeData of V,A by Def6;

take e ; :: thesis: ( e is Function-like & e is Relation-like )

thus ( e is Function-like & e is Relation-like ) ; :: thesis: verum

then reconsider e = {} as TypeSCNominativeData of V,A by Def6;

take e ; :: thesis: ( e is Function-like & e is Relation-like )

thus ( e is Function-like & e is Relation-like ) ; :: thesis: verum