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