let x be Element of G . s; :: thesis: ( x is Relation-like & x is Function-like )
( G . s c= the Sorts of (Free (S,X)) . s & x in G . s ) by PBOOLE:def 2, PBOOLE:def 18;
hence ( x is Relation-like & x is Function-like ) ; :: thesis: verum