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) /\ (Affin B) = conv B
let A be affinely-independent Subset of V; :: thesis: for B being Subset of V st B c= A holds
(conv A) /\ (Affin B) = conv B
let B be Subset of V; :: thesis: ( B c= A implies (conv A) /\ (Affin B) = conv B )
A1: conv B c= Affin B by RLAFFIN1:65;
assume A2: B c= A ; :: thesis: (conv A) /\ (Affin B) = conv B
thus (conv A) /\ (Affin B) c= conv B :: according to XBOOLE_0:def 10 :: thesis: conv B c= (conv A) /\ (Affin B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (conv A) /\ (Affin B) or x in conv B )
assume A3: x in (conv A) /\ (Affin B) ; :: thesis: x in conv B
then A4: x in Affin B by XBOOLE_0:def 4;
A5: x in conv A by A3, XBOOLE_0:def 4;

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 A2, A4, RLAFFIN1:77;
hence ( v in B implies 0 <= (x |-- B) . v ) by A5, RLAFFIN1:71; :: thesis: verum

end;

B is affinely-independent by A2, RLAFFIN1:43;
hence x in conv B by A4, A6, RLAFFIN1:73; :: thesis: verum

end;

conv B c= conv A by A2, RLAFFIN1:3;
hence conv B c= (conv A) /\ (Affin B) by A1, XBOOLE_1:19; :: thesis: verum