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 object ; :: 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 y9 = y as Element of A ;
( 0 < (MemberFunc (X,A)) . y9 & (MemberFunc (X,A)) . y9 < 1 ) by A1, Th42;
hence y in { x where x is Element of A : ( 0 < (MemberFunc (X,A)) . x & (MemberFunc (X,A)) . x < 1 ) } ; :: thesis: verum

end;

let y be object ; :: 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 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; :: thesis: verum