reconsider e = {} as PartFunc of REAL, the carrier of S by RELSET_1:25;
take e ; :: thesis: e is empty
thus e is empty ; :: thesis: verum