let a be FinSequence; :: thesis: {a} is relation
for z being object st z in {a} holds
z is FinSequence by TARSKI:def 1;
then reconsider X = {a} as FinSequence-membered set by FINSEQ_1:def 18;
X is with_common_domain ;
hence {a} is relation ; :: thesis: verum