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 )

proof

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;

assume w in (UncertaintyMap R) . u ; :: thesis: [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