let D be non empty set ; :: thesis: empty_rel D = {}
assume A1: not empty_rel D = {} ; :: thesis: contradiction
set x = the Element of empty_rel D;
empty_rel D is Subset of (D *) by Def7;
then the Element of empty_rel D in D * by A1, TARSKI:def 3;
then reconsider a = the Element of empty_rel D as FinSequence of D by FINSEQ_1:def 11;
a in empty_rel D by A1;
hence contradiction by Def9; :: thesis: verum