let R be non empty RelStr ; :: thesis: ( R is reflexive implies for w being Element of R holds w in (UncertaintyMap R) . w )
assume aa: R is reflexive ; :: thesis: for w being Element of R holds w in (UncertaintyMap R) . w
let w be Element of R; :: thesis: w in (UncertaintyMap R) . w
[w,w] in the InternalRel of R by aa, LATTAD_1:1;
hence w in (UncertaintyMap R) . w by For3; :: thesis: verum