take the empty PartFunc of REAL, the carrier of S ; :: thesis: the empty PartFunc of REAL, the carrier of S is empty
thus the empty PartFunc of REAL, the carrier of S is empty ; :: thesis: verum