let A be finite Approximation_Space; for X being Subset of A holds BndAp X = { x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) }
let X be Subset of A; BndAp X = { x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) }
thus
BndAp X c= { x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) }
XBOOLE_0:def 10 { x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) } c= BndAp X
let y be object ; TARSKI:def 3 ( not y in { x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) } or y in BndAp X )
assume
y in { x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) }
; y in BndAp X
then
ex y9 being Element of A st
( y9 = y & 0 < (MemberFunc (X,A)) . y9 & (MemberFunc (X,A)) . y9 < 1 )
;
hence
y in BndAp X
by Th42; verum