let R be finite Approximation_Space; :: thesis: for u being Element of R
for x, y being Subset of R st u in (Flip (f_1 R)) . x & (UncertaintyMap R) . u = y holds
kappa (y,x) = 1
let u be Element of R; :: thesis: for x, y being Subset of R st u in (Flip (f_1 R)) . x & (UncertaintyMap R) . u = y holds
kappa (y,x) = 1
let x, y be Subset of R; :: thesis: ( u in (Flip (f_1 R)) . x & (UncertaintyMap R) . u = y implies kappa (y,x) = 1 )
assume A0: ( u in (Flip (f_1 R)) . x & (UncertaintyMap R) . u = y ) ; :: thesis: kappa (y,x) = 1
(Flip (f_1 R)) . x = { w where w is Element of R : (UncertaintyMap R) . w c= x } by ROUGHS_5:30;
then consider v being Element of R such that
A3: ( u = v & (UncertaintyMap R) . v c= x ) by A0;
thus kappa (y,x) = 1 by Prop1a, A0, A3; :: thesis: verum