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 )

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

( [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
u in (tau R) . w
; :: thesis: [w,u] in the InternalRel of R
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;then u in Im ( the InternalRel of R,w) by RELAT_1:169;

hence u in (tau R) . w by DefTau; :: thesis: verum

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