let n be zero Nat; :: thesis: for X being non empty set
for r being Relation of X holds n -placesOf r is total symmetric transitive Relation of (n -tuples_on X)
let X be non empty set ; :: thesis: for r being Relation of X holds n -placesOf r is total symmetric transitive Relation of (n -tuples_on X)
let r be Relation of X; :: thesis: n -placesOf r is total symmetric transitive Relation of (n -tuples_on X)
set R = n -placesOf r;
Z0: n -tuples_on X = {(<*> X)} by FINSEQ_2:94
.= {{}} ;

now

let x be set ; :: thesis: ( x in n -tuples_on X implies ex y being set st [x,y] in n -placesOf r )
assume x in n -tuples_on X ; :: thesis: ex y being set st [x,y] in n -placesOf r
then x = {} by Z0;
then [x,x] in n -placesOf r by TARSKI:def 1;
hence ex y being set st [x,y] in n -placesOf r ; :: thesis: verum

end;

then Z11: dom (n -placesOf r) = n -tuples_on X by RELSET_1:9;
then n -placesOf r is total by PARTFUN1:def 2;
then B2: field (n -placesOf r) = n -tuples_on X by ORDERS_1:12;

now

let x, y be set ; :: thesis: ( x in n -tuples_on X & y in n -tuples_on X & [x,y] in n -placesOf r implies [y,x] in n -placesOf r )
assume x in n -tuples_on X ; :: thesis: ( y in n -tuples_on X & [x,y] in n -placesOf r implies [y,x] in n -placesOf r )
then C1: x = {} by Z0;
assume y in n -tuples_on X ; :: thesis: ( [x,y] in n -placesOf r implies [y,x] in n -placesOf r )
then C2: y = {} by Z0;
assume [x,y] in n -placesOf r ; :: thesis: [y,x] in n -placesOf r
thus [y,x] in n -placesOf r by C1, C2, TARSKI:def 1; :: thesis: verum

end;

then Z12: n -placesOf r is_symmetric_in n -tuples_on X by RELAT_2:def 3;
for x, y, z being set st x in n -tuples_on X & y in n -tuples_on X & z in n -tuples_on X & [x,y] in n -placesOf r & [y,z] in n -placesOf r holds
[x,z] in n -placesOf r by Z0;
then Z13: n -placesOf r is_transitive_in n -tuples_on X by RELAT_2:def 8;
thus n -placesOf r is total symmetric transitive Relation of (n -tuples_on X) by Z11, Z12, B2, Z13, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum