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 (R ~ ) * (P ~ ) ; :: thesis: [a,b] in (P * R) ~
then consider y being set such that
A2: ( [a,y] in R ~ & [y,b] in P ~ ) by Def8;
( [y,a] in R & [b,y] in P ) by A2, Def7;
then [b,a] in P * R by Def8;
hence [a,b] in (P * R) ~ by Def7; :: thesis: verum

end;

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
A3: ( [b,y] in P & [y,a] in R ) by Def8;
( [y,b] in P ~ & [a,y] in R ~ ) by A3, Def7;
hence [a,b] in (R ~ ) * (P ~ ) by Def8; :: 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