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)

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

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

conv B c= conv A
by A2, RLAFFIN1:3;
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;

hence x in conv B by A4, A6, RLAFFIN1:73; :: thesis: verum

end;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

B is affinely-independent
by A2, RLAFFIN1:43;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;x |-- B = x |-- A by A2, A4, RLAFFIN1:77;

hence ( v in B implies 0 <= (x |-- B) . v ) by A5, RLAFFIN1:71; :: thesis: verum

hence x in conv B by A4, A6, RLAFFIN1:73; :: thesis: verum

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