let A be finite Approximation_Space; :: thesis: for X being Subset of A
for x being Element of A holds
( ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) iff x in BndAp X )
let X be Subset of A; :: thesis: for x being Element of A holds
( ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) iff x in BndAp X )
let x be Element of A; :: thesis: ( ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) iff x in BndAp X )

hereby :: thesis: ( x in BndAp X implies ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) )

assume A1: ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) ; :: thesis: x in BndAp X
then not x in (UAp X) ` by Th41;
then ( x in UAp X & not x in LAp X ) by A1, Th40, XBOOLE_0:def 5;
hence x in BndAp X by XBOOLE_0:def 5; :: thesis: verum

end;

A2: ( 0 <= (MemberFunc X,A) . x & (MemberFunc X,A) . x <= 1 ) by Th38;
assume x in BndAp X ; :: thesis: ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 )
then A3: ( x in UAp X & not x in LAp X ) by XBOOLE_0:def 5;
then ( not x in (UAp X) ` & not x in LAp X ) by XBOOLE_0:def 5;
then A4: 0 <> (MemberFunc X,A) . x by Th41;
(MemberFunc X,A) . x <> 1 by A3, Th40;
hence ( 0 < (MemberFunc X,A) . x & (MemberFunc X,A) . x < 1 ) by A2, A4, XXREAL_0:1; :: thesis: verum