let V be RealLinearSpace; :: thesis: for A being affinely-independent Subset of V
for B being Subset of V st B c= A holds
(conv A) /\ () = conv B

let A be affinely-independent Subset of V; :: thesis: for B being Subset of V st B c= A holds
(conv A) /\ () = conv B

let B be Subset of V; :: thesis: ( B c= A implies (conv A) /\ () = conv B )
A1: conv B c= Affin B by RLAFFIN1:65;
assume A2: B c= A ; :: thesis: (conv A) /\ () = conv B
thus (conv A) /\ () c= conv B :: according to XBOOLE_0:def 10 :: thesis: conv B c= (conv A) /\ ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (conv A) /\ () or x in conv B )
assume A3: x in (conv A) /\ () ; :: thesis: x in conv B
then A4: x in Affin B by XBOOLE_0:def 4;
A5: x in conv A by ;
A6: now :: thesis: for v being Element of V st v in B holds
0 <= (x |-- B) . v
let v be Element of V; :: thesis: ( v in B implies 0 <= (x |-- B) . v )
x |-- B = x |-- A by ;
hence ( v in B implies 0 <= (x |-- B) . v ) by ; :: thesis: verum
end;
B is affinely-independent by ;
hence x in conv B by ; :: thesis: verum
end;
conv B c= conv A by ;
hence conv B c= (conv A) /\ () by ; :: thesis: verum