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