let R be non empty RelStr ; :: thesis: for u, w being Element of R holds

( u in Im ( the InternalRel of R,w) iff w in Coim ( the InternalRel of R,u) )

let u, w be Element of R; :: thesis: ( u in Im ( the InternalRel of R,w) iff w in Coim ( the InternalRel of R,u) )

thus ( u in Im ( the InternalRel of R,w) implies w in Coim ( the InternalRel of R,u) ) :: thesis: ( w in Coim ( the InternalRel of R,u) implies u in Im ( the InternalRel of R,w) )

then consider t being object such that

W1: ( [w,t] in the InternalRel of R & t in {u} ) by RELAT_1:def 14;

t = u by W1, TARSKI:def 1;

hence u in Im ( the InternalRel of R,w) by RELAT_1:169, W1; :: thesis: verum

( u in Im ( the InternalRel of R,w) iff w in Coim ( the InternalRel of R,u) )

let u, w be Element of R; :: thesis: ( u in Im ( the InternalRel of R,w) iff w in Coim ( the InternalRel of R,u) )

thus ( u in Im ( the InternalRel of R,w) implies w in Coim ( the InternalRel of R,u) ) :: thesis: ( w in Coim ( the InternalRel of R,u) implies u in Im ( the InternalRel of R,w) )

proof

assume
w in Coim ( the InternalRel of R,u)
; :: thesis: u in Im ( the InternalRel of R,w)
assume
u in Im ( the InternalRel of R,w)
; :: thesis: w in Coim ( the InternalRel of R,u)

then Z1: [w,u] in the InternalRel of R by RELAT_1:169;

u in {u} by TARSKI:def 1;

hence w in Coim ( the InternalRel of R,u) by Z1, RELAT_1:def 14; :: thesis: verum

end;then Z1: [w,u] in the InternalRel of R by RELAT_1:169;

u in {u} by TARSKI:def 1;

hence w in Coim ( the InternalRel of R,u) by Z1, RELAT_1:def 14; :: thesis: verum

then consider t being object such that

W1: ( [w,t] in the InternalRel of R & t in {u} ) by RELAT_1:def 14;

t = u by W1, TARSKI:def 1;

hence u in Im ( the InternalRel of R,w) by RELAT_1:169, W1; :: thesis: verum