thus k `11 is Element of commaObjs (F,G) ; :: thesis: verum