let n be Nat; :: thesis: for Ar being Subset of (REAL-NS n)
for At being Subset of (TOP-REAL n) st Ar = At holds
( Ar is Affine iff At is Affine )
let Ar be Subset of (REAL-NS n); :: thesis: for At being Subset of (TOP-REAL n) st Ar = At holds
( Ar is Affine iff At is Affine )
let At be Subset of (TOP-REAL n); :: thesis: ( Ar = At implies ( Ar is Affine iff At is Affine ) )
assume A1: Ar = At ; :: thesis: ( Ar is Affine iff At is Affine )

hereby :: thesis: ( At is Affine implies Ar is Affine )

assume A2: Ar is Affine ; :: thesis: At is Affine
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: for a being Real st x in At & y in At holds
((1 - a) * x) + (a * y) in At
let a be Real; :: thesis: ( x in At & y in At implies ((1 - a) * x) + (a * y) in At )
assume A3: ( x in At & y in At ) ; :: thesis: ((1 - a) * x) + (a * y) in At
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: verum

end;

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

end;

assume A4: At is Affine ; :: thesis: Ar is Affine
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: for a being Real st x in Ar & y in Ar holds
((1 - a) * x) + (a * y) in Ar
let a be Real; :: thesis: ( x in Ar & y in Ar implies ((1 - a) * x) + (a * y) in Ar )
assume A5: ( x in Ar & y in Ar ) ; :: thesis: ((1 - a) * x) + (a * y) in Ar
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: verum

end;

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