let n be zero Nat; :: thesis: for X being non empty set
for r being Relation of X holds
( n -placesOf r is total & n -placesOf r is symmetric & n -placesOf r is transitive )
let X be non empty set ; :: thesis: for r being Relation of X holds
( n -placesOf r is total & n -placesOf r is symmetric & n -placesOf r is transitive )
let r be Relation of X; :: thesis: ( n -placesOf r is total & n -placesOf r is symmetric & n -placesOf r is transitive )
set R = n -placesOf r;

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

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

end;

then dom (n -placesOf r) = n -tuples_on X by RELSET_1:9;
hence n -placesOf r is total by PARTFUN1:def 2; :: thesis: ( n -placesOf r is symmetric & n -placesOf r is transitive )
then A1: field (n -placesOf r) = n -tuples_on X by ORDERS_1:12;
thus n -placesOf r is symmetric :: thesis: n -placesOf r is transitive

proof

let x, y be object ; :: according to RELAT_2:def 3,RELAT_2:def 11 :: thesis: ( not x in field (n -placesOf r) or not y in field (n -placesOf r) or not [x,y] in n -placesOf r or [y,x] in n -placesOf r )
assume x in field (n -placesOf r) ; :: thesis: ( not y in field (n -placesOf r) or not [x,y] in n -placesOf r or [y,x] in n -placesOf r )
then A2: x = {} by A1;
assume y in field (n -placesOf r) ; :: thesis: ( not [x,y] in n -placesOf r or [y,x] in n -placesOf r )
then A3: y = {} by A1;
assume [x,y] in n -placesOf r ; :: thesis: [y,x] in n -placesOf r
thus [y,x] in n -placesOf r by TARSKI:def 1, A2, A3; :: thesis: verum

end;

A4: for x, y, z being object 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 ;
thus n -placesOf r is transitive by A4, A1, RELAT_2:def 8; :: thesis: verum