let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the Sorts of (Free (C,(MSVars C))) . (a_Term C) or x in Union the Sorts of (Free (C,(MSVars C))) )
dom the Sorts of (Free (C,(MSVars C))) = the carrier of C by PARTFUN1:def 2;
hence ( not x in the Sorts of (Free (C,(MSVars C))) . (a_Term C) or x in Union the Sorts of (Free (C,(MSVars C))) ) by CARD_5:2; :: thesis: verum