let a be Element of A0,s; :: thesis: ( a is Function-like & a is Relation-like )
a is Element of the Sorts of A0 . s ;
hence ( a is Function-like & a is Relation-like ) ; :: thesis: verum