set BB = { B where B is Affine Subset of RLS : A c= B } ;
let v1, v2 be Element of RLS; :: according to RUSUB_4:def 4 :: thesis: for b1 being object holds
( not v1 in Affin A or not v2 in Affin A or ((1 - b1) * v1) + (b1 * v2) in Affin A )
let r be Real; :: thesis: ( not v1 in Affin A or not v2 in Affin A or ((1 - r) * v1) + (r * v2) in Affin A )
assume that
A1: v1 in Affin A and
A2: v2 in Affin A ; :: thesis: ((1 - r) * v1) + (r * v2) in Affin A
A3: now :: thesis: for Y being set st Y in { B where B is Affine Subset of RLS : A c= B } holds
((1 - r) * v1) + (r * v2) in Y
let Y be set ; :: thesis: ( Y in { B where B is Affine Subset of RLS : A c= B } implies ((1 - r) * v1) + (r * v2) in Y )
assume A4: Y in { B where B is Affine Subset of RLS : A c= B } ; :: thesis: ((1 - r) * v1) + (r * v2) in Y
then consider B being Affine Subset of RLS such that
A5: Y = B and
A c= B ;
( v1 in B & v2 in B ) by A1, A2, A4, A5, SETFAM_1:def 1;
hence ((1 - r) * v1) + (r * v2) in Y by A5, RUSUB_4:def 4; :: thesis: verum
end;
{ B where B is Affine Subset of RLS : A c= B } <> {} by A1, SETFAM_1:def 1;
hence ((1 - r) * v1) + (r * v2) in Affin A by A3, SETFAM_1:def 1; :: thesis: verum