let P, R be Relation; :: thesis: ( P = (rng P) | R iff P ~ = (R ~ ) | (dom (P ~ )) )

hereby :: thesis: ( P ~ = (R ~ ) | (dom (P ~ )) implies P = (rng P) | R )

assume A1: P = (rng P) | R ; :: thesis: P ~ = (R ~ ) | (dom (P ~ ))

now

let x, y be set ; :: thesis: ( ( [x,y] in P ~ implies [x,y] in (R ~ ) | (dom (P ~ )) ) & ( [x,y] in (R ~ ) | (dom (P ~ )) implies [x,y] in P ~ ) )

hereby :: thesis: ( [x,y] in (R ~ ) | (dom (P ~ )) implies [x,y] in P ~ )

assume A2: [x,y] in P ~ ; :: thesis: [x,y] in (R ~ ) | (dom (P ~ ))
then [y,x] in P by RELAT_1:def 7;
then ( x in rng P & [y,x] in R ) by A1, RELAT_1:def 12;
then ( x in dom (P ~ ) & [x,y] in R ~ ) by A2, RELAT_1:def 4, RELAT_1:def 7;
hence [x,y] in (R ~ ) | (dom (P ~ )) by RELAT_1:def 11; :: thesis: verum

end;

assume [x,y] in (R ~ ) | (dom (P ~ )) ; :: thesis: [x,y] in P ~
then ( x in dom (P ~ ) & [x,y] in R ~ ) by RELAT_1:def 11;
then ( x in rng P & [y,x] in R ) by RELAT_1:37, RELAT_1:def 7;
then [y,x] in (rng P) | R by RELAT_1:def 12;
hence [x,y] in P ~ by A1, RELAT_1:def 7; :: thesis: verum

end;

hence P ~ = (R ~ ) | (dom (P ~ )) by RELAT_1:def 2; :: thesis: verum

end;

assume A3: P ~ = (R ~ ) | (dom (P ~ )) ; :: thesis: P = (rng P) | R

now

let x, y be set ; :: thesis: ( ( [x,y] in P implies [x,y] in (rng P) | R ) & ( [x,y] in (rng P) | R implies [x,y] in P ) )

hereby :: thesis: ( [x,y] in (rng P) | R implies [x,y] in P )

assume [x,y] in P ; :: thesis: [x,y] in (rng P) | R
then [y,x] in P ~ by RELAT_1:def 7;
then ( y in dom (P ~ ) & [y,x] in R ~ ) by A3, RELAT_1:def 11;
then ( y in rng P & [x,y] in R ) by RELAT_1:37, RELAT_1:def 7;
hence [x,y] in (rng P) | R by RELAT_1:def 12; :: thesis: verum

end;

assume [x,y] in (rng P) | R ; :: thesis: [x,y] in P
then ( y in rng P & [x,y] in R ) by RELAT_1:def 12;
then ( y in dom (P ~ ) & [y,x] in R ~ ) by RELAT_1:37, RELAT_1:def 7;
then [y,x] in (R ~ ) | (dom (P ~ )) by RELAT_1:def 11;
hence [x,y] in P by A3, RELAT_1:def 7; :: thesis: verum

end;

hence P = (rng P) | R by RELAT_1:def 2; :: thesis: verum