let D be non empty set ; :: thesis: for x, y being Element of D holds {<*x,y*>} is Element of relations_on D
let x, y be Element of D; :: thesis: {<*x,y*>} is Element of relations_on D
{<*x,y*>} in relations_on D

proof

<*x*> ^ <*y*> is FinSequence of D ;
then <*x,y*> is FinSequence of D by FINSEQ_1:def 9;
then <*x,y*> in D * by FINSEQ_1:def 11;
then A1: {<*x,y*>} c= D * by ZFMISC_1:37;
for a1, a2 being FinSequence of D st a1 in {<*x,y*>} & a2 in {<*x,y*>} holds
len a1 = len a2

proof

let a1, a2 be FinSequence of D; :: thesis: ( a1 in {<*x,y*>} & a2 in {<*x,y*>} implies len a1 = len a2 )
assume ( a1 in {<*x,y*>} & a2 in {<*x,y*>} ) ; :: thesis: len a1 = len a2
then ( a1 = <*x,y*> & a2 = <*x,y*> ) by TARSKI:def 1;
hence len a1 = len a2 ; :: thesis: verum

end;

hence {<*x,y*>} in relations_on D by A1, Def8; :: thesis: verum

end;

hence {<*x,y*>} is Element of relations_on D ; :: thesis: verum