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 that
A1: 0 < (MemberFunc X,A) . x and
A2: (MemberFunc X,A) . x < 1 ; :: thesis: x in BndAp X
not x in (UAp X) ` by A1, Th41;
then A3: x in UAp X by XBOOLE_0:def 5;
not x in LAp X by A2, Th40;
hence x in BndAp X by A3, XBOOLE_0:def 5; :: thesis: verum

end;

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