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

( [w,u] in the InternalRel of R iff w in (UncertaintyMap R) . u )

let w, u be Element of R; :: thesis: ( [w,u] in the InternalRel of R iff w in (UncertaintyMap R) . u )

thus ( [w,u] in the InternalRel of R implies w in (UncertaintyMap R) . u ) :: thesis: ( w in (UncertaintyMap R) . u implies [w,u] in the InternalRel of R )

then w in Coim ( the InternalRel of R,u) by DefUnc;

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 w in (UncertaintyMap R) . u )

let w, u be Element of R; :: thesis: ( [w,u] in the InternalRel of R iff w in (UncertaintyMap R) . u )

thus ( [w,u] in the InternalRel of R implies w in (UncertaintyMap R) . u ) :: thesis: ( w in (UncertaintyMap R) . u implies [w,u] in the InternalRel of R )

proof

assume
w in (UncertaintyMap R) . u
; :: thesis: [w,u] in the InternalRel of R
assume S1:
[w,u] in the InternalRel of R
; :: thesis: w in (UncertaintyMap R) . u

u in {u} by TARSKI:def 1;

then w in Coim ( the InternalRel of R,u) by S1, RELAT_1:def 14;

hence w in (UncertaintyMap R) . u by DefUnc; :: thesis: verum

end;u in {u} by TARSKI:def 1;

then w in Coim ( the InternalRel of R,u) by S1, RELAT_1:def 14;

hence w in (UncertaintyMap R) . u by DefUnc; :: thesis: verum

then w in Coim ( the InternalRel of R,u) by DefUnc;

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