let n be Nat; :: thesis:
let Ar be Subset of (REAL-NS n); :: thesis:
let At be Subset of (TOP-REAL n); :: thesis:
assume A1: Ar = At ; :: thesis:

hereby :: thesis:

assume A2: Ar is Affine ; :: thesis:
for x, y being VECTOR of (TOP-REAL n)
for a being Real st x in At & y in At holds
((1 - a) * x) + (a * y) in At

proof

let x, y be VECTOR of (TOP-REAL n); :: thesis:
let a be Real; :: thesis:
assume A3: ( x in At & y in At ) ; :: thesis:
reconsider x0 = x, y0 = y as VECTOR of (REAL-NS n) by Th4;
( (1 - a) * x = (1 - a) * x0 & a * y = a * y0 ) by Th8;
then ((1 - a) * x) + (a * y) = ((1 - a) * x0) + (a * y0) by Th7;
hence ((1 - a) * x) + (a * y) in At by A1, A2, A3, RUSUB_4:def 4; :: thesis:

end;

hence At is Affine by RUSUB_4:def 4; :: thesis:

end;

assume A4: At is Affine ; :: thesis:
for x, y being VECTOR of (REAL-NS n)
for a being Real st x in Ar & y in Ar holds
((1 - a) * x) + (a * y) in Ar

proof

let x, y be VECTOR of (REAL-NS n); :: thesis:
let a be Real; :: thesis:
assume A5: ( x in Ar & y in Ar ) ; :: thesis:
reconsider x0 = x, y0 = y as VECTOR of (TOP-REAL n) by Th4;
( (1 - a) * x = (1 - a) * x0 & a * y = a * y0 ) by Th8;
then ((1 - a) * x) + (a * y) = ((1 - a) * x0) + (a * y0) by Th7;
hence ((1 - a) * x) + (a * y) in Ar by A1, A4, A5, RUSUB_4:def 4; :: thesis:

end;

hence Ar is Affine by RUSUB_4:def 4; :: thesis: