let RLS be non empty RLSStruct ; :: thesis: for A, B being Subset of RLS st A c= B holds
conv A c= conv B
let A, B be Subset of RLS; :: thesis: ( A c= B implies conv A c= conv B )
assume A1: A c= B ; :: thesis: conv A c= conv B
A2: Convex-Family B c= Convex-Family A

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Convex-Family B or x in Convex-Family A )
assume A3: x in Convex-Family B ; :: thesis: x in Convex-Family A
then reconsider X = x as Subset of RLS ;
B c= X by A3, CONVEX1:def 4;
then A4: A c= X by A1;
X is convex by A3, CONVEX1:def 4;
hence x in Convex-Family A by A4, CONVEX1:def 4; :: thesis: verum

end;

[#] RLS is convex ;
then [#] RLS in Convex-Family B by CONVEX1:def 4;
then A5: meet (Convex-Family A) c= meet (Convex-Family B) by A2, SETFAM_1:6;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in conv A or y in conv B )
assume y in conv A ; :: thesis: y in conv B
hence y in conv B by A5; :: thesis: verum