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