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;

now :: thesis: for x being set st x in n -tuples_on X holds
ex y being set st [x,y] in n -placesOf r

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 = {} ;
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 A1: dom (n -placesOf r) = n -tuples_on X by RELSET_1:9;
then n -placesOf r is total by PARTFUN1:def 2;
then A2: field (n -placesOf r) = n -tuples_on X by ORDERS_1:12;

now :: thesis: for x, y being set st x in n -tuples_on X & y in n -tuples_on X & [x,y] in n -placesOf r holds
[y,x] in n -placesOf r

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 A3: x = {} ;
assume y in n -tuples_on X ; :: thesis: ( [x,y] in n -placesOf r implies [y,x] in n -placesOf r )
then A4: y = {} ;
assume [x,y] in n -placesOf r ; :: thesis: [y,x] in n -placesOf r
thus [y,x] in n -placesOf r by A3, A4, TARSKI:def 1; :: thesis: verum

end;

then A5: 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 ;
then A6: 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 A1, A5, A2, A6, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; :: thesis: verum