let P, R be Relation; ( P = (rng P) |` R iff P ~ = (R ~) | (dom (P ~)) )
hereby ( P ~ = (R ~) | (dom (P ~)) implies P = (rng P) |` R )
assume A1:
P = (rng P) |` R
;
P ~ = (R ~) | (dom (P ~))now for x, y being object holds
( ( [x,y] in P ~ implies [x,y] in (R ~) | (dom (P ~)) ) & ( [x,y] in (R ~) | (dom (P ~)) implies [x,y] in P ~ ) )let x,
y be
object ;
( ( [x,y] in P ~ implies [x,y] in (R ~) | (dom (P ~)) ) & ( [x,y] in (R ~) | (dom (P ~)) implies [x,y] in P ~ ) )assume A4:
[x,y] in (R ~) | (dom (P ~))
;
[x,y] in P ~ then
[x,y] in R ~
by RELAT_1:def 11;
then A5:
[y,x] in R
by RELAT_1:def 7;
x in dom (P ~)
by A4, RELAT_1:def 11;
then
x in rng P
by RELAT_1:20;
then
[y,x] in (rng P) |` R
by A5, RELAT_1:def 12;
hence
[x,y] in P ~
by A1, RELAT_1:def 7;
verum end; hence
P ~ = (R ~) | (dom (P ~))
;
verum
end;
assume A6:
P ~ = (R ~) | (dom (P ~))
; P = (rng P) |` R
now for x, y being object holds
( ( [x,y] in P implies [x,y] in (rng P) |` R ) & ( [x,y] in (rng P) |` R implies [x,y] in P ) )let x,
y be
object ;
( ( [x,y] in P implies [x,y] in (rng P) |` R ) & ( [x,y] in (rng P) |` R implies [x,y] in P ) )hereby ( [x,y] in (rng P) |` R implies [x,y] in P )
assume
[x,y] in P
;
[x,y] in (rng P) |` Rthen A7:
[y,x] in P ~
by RELAT_1:def 7;
then
[y,x] in R ~
by A6, RELAT_1:def 11;
then A8:
[x,y] in R
by RELAT_1:def 7;
y in dom (P ~)
by A6, A7, RELAT_1:def 11;
then
y in rng P
by RELAT_1:20;
hence
[x,y] in (rng P) |` R
by A8, RELAT_1:def 12;
verum
end; assume A9:
[x,y] in (rng P) |` R
;
[x,y] in Pthen
[x,y] in R
by RELAT_1:def 12;
then A10:
[y,x] in R ~
by RELAT_1:def 7;
y in rng P
by A9, RELAT_1:def 12;
then
y in dom (P ~)
by RELAT_1:20;
then
[y,x] in (R ~) | (dom (P ~))
by A10, RELAT_1:def 11;
hence
[x,y] in P
by A6, RELAT_1:def 7;
verum end;
hence
P = (rng P) |` R
; verum