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) )

proof

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;

assume w in Coim ( the InternalRel of R,u) ; :: thesis: 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