let R be non empty RelStr ; :: thesis: for w, u being Element of R holds
( [w,u] in the InternalRel of R iff u in (tau R) . w )
let w, u be Element of R; :: thesis: ( [w,u] in the InternalRel of R iff u in (tau R) . w )
thus ( [w,u] in the InternalRel of R implies u in (tau R) . w ) :: thesis: ( u in (tau R) . w implies [w,u] in the InternalRel of R )

proof

assume [w,u] in the InternalRel of R ; :: thesis: u in (tau R) . w
then u in Im ( the InternalRel of R,w) by RELAT_1:169;
hence u in (tau R) . w by DefTau; :: thesis: verum

end;

assume u in (tau R) . w ; :: thesis: [w,u] in the InternalRel of R
then u in Im ( the InternalRel of R,w) by DefTau;
then w in Coim ( the InternalRel of R,u) by ImCoim;
then consider x being object such that
S1: ( [w,x] in the InternalRel of R & x in {u} ) by RELAT_1:def 14;
thus [w,u] in the InternalRel of R by S1, TARSKI:def 1; :: thesis: verum