let R be non empty RelStr ; :: thesis: ( the InternalRel of R is symmetric implies UncertaintyMap R = tau R )
assume AA: the InternalRel of R is symmetric ; :: thesis:
set f = UncertaintyMap R;
set g = tau R;
for x being Element of R holds () . x = (tau R) . x
proof
let x be Element of R; :: thesis: () . x = (tau R) . x
Z2: (UncertaintyMap R) . x = Coim ( the InternalRel of R,x) by DefUnc;
ZZ: Im ( the InternalRel of R,x) c= Coim ( the InternalRel of R,x)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Im ( the InternalRel of R,x) or y in Coim ( the InternalRel of R,x) )
assume y in Im ( the InternalRel of R,x) ; :: thesis: y in Coim ( the InternalRel of R,x)
then [x,y] in the InternalRel of R by RELAT_1:169;
then B2: [y,x] in the InternalRel of R by ;
x in {x} by TARSKI:def 1;
hence y in Coim ( the InternalRel of R,x) by ; :: thesis: verum
end;
Coim ( the InternalRel of R,x) c= Im ( the InternalRel of R,x)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Coim ( the InternalRel of R,x) or y in Im ( the InternalRel of R,x) )
assume y in Coim ( the InternalRel of R,x) ; :: thesis: y in Im ( the InternalRel of R,x)
then consider yy being object such that
B2: ( [y,yy] in the InternalRel of R & yy in {x} ) by RELAT_1:def 14;
yy = x by ;
then [x,y] in the InternalRel of R by ;
hence y in Im ( the InternalRel of R,x) by RELAT_1:169; :: thesis: verum
end;
hence (UncertaintyMap R) . x = (tau R) . x by ; :: thesis: verum
end;
hence UncertaintyMap R = tau R ; :: thesis: verum