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))
( (MemberFunc ((X /\ Y),A)) . x <= (MemberFunc (X,A)) . x & (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 XXREAL_0:20; :: thesis: verum