let P, R be Relation; :: thesis: (P * R) ~ = (R ~ ) * (P ~ )
let a be set ; :: according to RELAT_1:def 2 :: thesis: for b being set holds
( [a,b] in (P * R) ~ iff [a,b] in (R ~ ) * (P ~ ) )
let b be set ; :: thesis: ( [a,b] in (P * R) ~ iff [a,b] in (R ~ ) * (P ~ ) )

hereby :: thesis: ( [a,b] in (R ~ ) * (P ~ ) implies [a,b] in (P * R) ~ )

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;

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