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

then [#] RLS in Convex-Family A by CONVEX1:def 4;

hence x in conv A by A2, SETFAM_1:def 1; :: thesis: verum

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

[#] RLS is convex
;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;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

then [#] RLS in Convex-Family A by CONVEX1:def 4;

hence x in conv A by A2, SETFAM_1:def 1; :: thesis: verum