the Element of F + the Element of G in F ++ G by Th39;
hence not F ++ G is empty ; :: thesis: verum