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