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:8;
hence not e is pair by Th5; :: thesis: verum