let A be finite Approximation_Space; :: thesis: for X, Y being Subset of A
for x being Element of A holds (MemberFunc (X /\ Y),A) . x <= min ((MemberFunc X,A) . x),((MemberFunc Y,A) . x)
let X, Y be Subset of A; :: thesis: for x being Element of A holds (MemberFunc (X /\ Y),A) . x <= min ((MemberFunc X,A) . x),((MemberFunc Y,A) . x)
let x be Element of A; :: thesis: (MemberFunc (X /\ Y),A) . x <= min ((MemberFunc X,A) . x),((MemberFunc Y,A) . x)
A1: (MemberFunc (X /\ Y),A) . x <= (MemberFunc X,A) . x by Th47, XBOOLE_1:17;
(MemberFunc (X /\ Y),A) . x <= (MemberFunc Y,A) . x by Th47, XBOOLE_1:17;
hence (MemberFunc (X /\ Y),A) . x <= min ((MemberFunc X,A) . x),((MemberFunc Y,A) . x) by A1, XXREAL_0:20; :: thesis: verum