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