let RLS be non empty RLSStruct ; :: thesis: for S, A being Subset of RLS st A c= conv S holds
conv S = conv (S \/ A)
let S, A be Subset of RLS; :: thesis: ( A c= conv S implies conv S = conv (S \/ A) )
assume A1: A c= conv S ; :: thesis: conv S = conv (S \/ A)
thus conv S c= conv (S \/ A) by Th3, XBOOLE_1:7; :: according to XBOOLE_0:def 10 :: thesis: conv (S \/ A) c= conv S
S c= conv S by Lm1;
then S \/ A c= conv S by A1, XBOOLE_1:8;
hence conv (S \/ A) c= conv S by CONVEX1:30; :: thesis: verum