let e be Element of (Free (S,X)); :: thesis: not e is pair
e is Term of S,(X \/ ( the carrier of S --> {0})) by MSAFREE3:9;
hence not e is pair by Th5; :: thesis: verum