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