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