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 >= max ((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 >= max ((MemberFunc X,A) . x),((MemberFunc Y,A) . x)
let x be Element of A; :: thesis: (MemberFunc (X \/ Y),A) . x >= max ((MemberFunc X,A) . x),((MemberFunc Y,A) . x)
A1: (MemberFunc (X \/ Y),A) . x >= (MemberFunc X,A) . x by Th47, XBOOLE_1:7;
(MemberFunc (X \/ Y),A) . x >= (MemberFunc Y,A) . x by Th47, XBOOLE_1:7;
hence (MemberFunc (X \/ Y),A) . x >= max ((MemberFunc X,A) . x),((MemberFunc Y,A) . x) by A1, XXREAL_0:28; :: thesis: verum