let R be Approximation_Space; :: thesis: for x being Subset of R holds (f_0 R) . x is exact

let x be Subset of R; :: thesis: (f_0 R) . x is exact

(f_0 R) . x = (UAp R) . x by UApF0

.= UAp x by ROUGHS_2:def 11 ;

hence (f_0 R) . x is exact ; :: thesis: verum

let x be Subset of R; :: thesis: (f_0 R) . x is exact

(f_0 R) . x = (UAp R) . x by UApF0

.= UAp x by ROUGHS_2:def 11 ;

hence (f_0 R) . x is exact ; :: thesis: verum