let A be finite Approximation_Space; :: thesis: for X being Subset of holds BndAp X = { x where x is Element of : ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) }
let X be Subset of ; :: thesis: BndAp X = { x where x is Element of : ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) }
thus BndAp X c= { x where x is Element of : ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) } :: according to XBOOLE_0:def 10 :: thesis: { x where x is Element of : ( 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 : ( 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 : ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) }
then reconsider y' = y as Element of ;
( 0 < (MemberFunc X,A) . y' & (MemberFunc X,A) . y' < 1 ) by A1, Th42;
hence y in { x where x is Element of : ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) } ; :: thesis: verum

end;

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