let P, R be Relation; :: thesis: (P * R) ~ = (R ~ ) * (P ~ )

now

let a, b be set ; :: thesis: ( [a,b] in (P * R) ~ iff [a,b] in (R ~ ) * (P ~ ) )

A1: now

assume [a,b] in (P * R) ~ ; :: thesis: [a,b] in (R ~ ) * (P ~ )
then [b,a] in P * R by Def7;
then consider y being set such that
A2: ( [b,y] in P & [y,a] in R ) by Def8;
A3: [y,b] in P ~ by A2, Def7;
[a,y] in R ~ by A2, Def7;
hence [a,b] in (R ~ ) * (P ~ ) by A3, Def8; :: thesis: verum

end;

now

assume [a,b] in (R ~ ) * (P ~ ) ; :: thesis: [a,b] in (P * R) ~
then consider y being set such that
A4: ( [a,y] in R ~ & [y,b] in P ~ ) by Def8;
A5: [y,a] in R by A4, Def7;
[b,y] in P by A4, Def7;
then [b,a] in P * R by A5, Def8;
hence [a,b] in (P * R) ~ by Def7; :: thesis: verum

end;

hence ( [a,b] in (P * R) ~ iff [a,b] in (R ~ ) * (P ~ ) ) by A1; :: thesis: verum

end;

hence (P * R) ~ = (R ~ ) * (P ~ ) by Def2; :: thesis: verum