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