[g,f] in the carrier of [:G,F:] ;
hence [g,f] is Element of [:G,F:] ; :: thesis: verum