let RLS be non empty RLSStruct ; :: thesis: for A being Subset of RLS holds A c= conv A
let A be Subset of RLS; :: thesis: A c= conv A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in conv A )
assume A1: x in A ; :: thesis: x in conv A
A2: now :: thesis: for y being set st y in Convex-Family A holds
x in y
let y be set ; :: thesis: ( y in Convex-Family A implies x in y )
assume y in Convex-Family A ; :: thesis: x in y
then A c= y by CONVEX1:def 4;
hence x in y by A1; :: thesis: verum
end;
[#] RLS is convex ;
then [#] RLS in Convex-Family A by CONVEX1:def 4;
hence x in conv A by A2, SETFAM_1:def 1; :: thesis: verum