let R be finite Approximation_Space; :: thesis: for u being Element of R
for x, y being Subset of R st u in (f_1 R) . x & (UncertaintyMap R) . u = y holds
kappa (y,x) > 0
let u be Element of R; :: thesis: for x, y being Subset of R st u in (f_1 R) . x & (UncertaintyMap R) . u = y holds
kappa (y,x) > 0
let x, y be Subset of R; :: thesis: ( u in (f_1 R) . x & (UncertaintyMap R) . u = y implies kappa (y,x) > 0 )
assume AA: ( u in (f_1 R) . x & (UncertaintyMap R) . u = y ) ; :: thesis: kappa (y,x) > 0
(f_1 R) . x = { u where u is Element of R : (UncertaintyMap R) . u meets x } by ROUGHS_5:def 5;
then consider uu being Element of R such that
AB: ( uu = u & (UncertaintyMap R) . uu meets x ) by AA;
kappa (y,x) <> 0 by AB, AA, LemmaProp2b;
hence kappa (y,x) > 0 by XXREAL_1:1; :: thesis: verum