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