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 b_{1} being object holds

( not v1 in Affin A or not v2 in Affin A or ((1 - b_{1}) * v1) + (b_{1} * 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

hence ((1 - r) * v1) + (r * v2) in Affin A by A3, SETFAM_1:def 1; :: thesis: verum

let v1, v2 be Element of RLS; :: according to RUSUB_4:def 4 :: thesis: for b

( not v1 in Affin A or not v2 in Affin A or ((1 - b

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

{ B where B is Affine Subset of RLS : A c= B } <> {}
by A1, SETFAM_1:def 1;((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;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

hence ((1 - r) * v1) + (r * v2) in Affin A by A3, SETFAM_1:def 1; :: thesis: verum