let U1, U2 be non empty set ; :: thesis: for n being Nat
for R being Relation of U1,U2 holds n -placesOf (R ~) = (n -placesOf R) ~
let n be Nat; :: thesis: for R being Relation of U1,U2 holds n -placesOf (R ~) = (n -placesOf R) ~
let R be Relation of U1,U2; :: thesis: n -placesOf (R ~) = (n -placesOf R) ~
set N1 = n -tuples_on U1;
set N2 = n -tuples_on U2;
set IT = { [q,p] where p is Element of n -tuples_on U1, q is Element of n -tuples_on U2 : for j being set st j in Seg n holds
[(p . j),(q . j)] in R } ;
reconsider Q = R ~ as Relation of U2,U1 ;
reconsider Rn = n -placesOf R as Relation of (n -tuples_on U1),(n -tuples_on U2) ;
reconsider LH = n -placesOf Q as Relation of (n -tuples_on U2),(n -tuples_on U1) ;
reconsider RH = Rn ~ as Relation of (n -tuples_on U2),(n -tuples_on U1) ;

now :: thesis: for x being object st x in LH holds
x in RH

let x be object ; :: thesis: ( x in LH implies x in RH )
assume x in LH ; :: thesis: x in RH
then consider p being Element of n -tuples_on U2, q being Element of n -tuples_on U1 such that
A1: ( x = [p,q] & ( for j being set st j in Seg n holds
[(p . j),(q . j)] in R ~ ) ) ;
for j being set st j in Seg n holds
[(q . j),(p . j)] in R

proof

let j be set ; :: thesis: ( j in Seg n implies [(q . j),(p . j)] in R )
assume j in Seg n ; :: thesis: [(q . j),(p . j)] in R
then [(p . j),(q . j)] in R ~ by A1;
hence [(q . j),(p . j)] in R by RELAT_1:def 7; :: thesis: verum

end;

then [q,p] in Rn ;
hence x in RH by RELAT_1:def 7, A1; :: thesis: verum

end;

then A2: LH c= RH by TARSKI:def 3;

now :: thesis: for x being object st x in RH ~ holds
x in LH ~

let x be object ; :: thesis: ( x in RH ~ implies x in LH ~ )
assume x in RH ~ ; :: thesis: x in LH ~
then consider p being Element of n -tuples_on U1, q being Element of n -tuples_on U2 such that
A3: ( x = [p,q] & ( for j being set st j in Seg n holds
[(p . j),(q . j)] in R ) ) ;
for j being set st j in Seg n holds
[(q . j),(p . j)] in R ~

proof

let j be set ; :: thesis: ( j in Seg n implies [(q . j),(p . j)] in R ~ )
assume j in Seg n ; :: thesis: [(q . j),(p . j)] in R ~
then [(p . j),(q . j)] in R by A3;
hence [(q . j),(p . j)] in R ~ by RELAT_1:def 7; :: thesis: verum

end;

then [q,p] in LH ;
hence x in LH ~ by A3, RELAT_1:def 7; :: thesis: verum

end;

then RH ~ c= LH ~ by TARSKI:def 3;
then (RH ~) \ (LH ~) = {} ;
then (RH \ LH) ~ = {} by RELAT_1:24;
then ((RH \ LH) ~) ~ = {} ;
then RH c= LH by XBOOLE_1:37;
hence n -placesOf (R ~) = (n -placesOf R) ~ by A2; :: thesis: verum