let A be finite Approximation_Space; :: thesis: 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; :: thesis: 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 ) } :: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of A : ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) } c= BndAp X

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in BndAp X or y in { x where x is Element of A : ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) } )
assume A1: y in BndAp X ; :: thesis: y in { x where x is Element of A : ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) }
then reconsider y' = y as Element of A ;
A2: 0 < (MemberFunc X,A) . y' by A1, Th42;
(MemberFunc X,A) . y' < 1 by A1, Th42;
hence y in { x where x is Element of A : ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) } by A2; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( 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 ) } ; :: thesis: y in BndAp X
then consider y' being Element of A such that
A3: ( y' = y & 0 < (MemberFunc X,A) . y' & (MemberFunc X,A) . y' < 1 ) ;
thus y in BndAp X by A3, Th42; :: thesis: verum