let S be set ; :: thesis: ( S is standard-ins implies S is Relation-like )
assume S is standard-ins ; :: thesis: S is Relation-like
then ex X being non empty set st S c= [:NAT,(NAT *),(X *):] by Def1;
hence S is Relation-like ; :: thesis: verum