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
Affin Ar = Affin At
let Ar be Subset of (REAL-NS n); :: thesis: for At being Subset of (TOP-REAL n) st Ar = At holds
Affin Ar = Affin At
let At be Subset of (TOP-REAL n); :: thesis: ( Ar = At implies Affin Ar = Affin At )
assume A1: Ar = At ; :: thesis: Affin Ar = Affin At
set AM = { B where B is Affine Subset of (REAL-NS n) : Ar c= B } ;
set BM = { B where B is Affine Subset of (TOP-REAL n) : At c= B } ;
A2: Affin Ar = meet { B where B is Affine Subset of (REAL-NS n) : Ar c= B } by RLAFFIN1:def 6;
A3: Affin At = meet { B where B is Affine Subset of (TOP-REAL n) : At c= B } by RLAFFIN1:def 6;
At c= Affin At by RLAFFIN1:49;
then A4: Affin At in { B where B is Affine Subset of (TOP-REAL n) : At c= B } ;
Ar c= Affin Ar by RLAFFIN1:49;
then A5: Affin Ar in { B where B is Affine Subset of (REAL-NS n) : Ar c= B } ;
for x being object holds
( x in Affin Ar iff x in Affin At )
proof
let x be object ; :: thesis: ( x in Affin Ar iff x in Affin At )
hereby :: thesis: ( x in Affin At implies x in Affin Ar )
assume A6: x in Affin Ar ; :: thesis: x in Affin At
now :: thesis: for Y being set st Y in { B where B is Affine Subset of (TOP-REAL n) : At c= B } holds
x in Y
let Y be set ; :: thesis: ( Y in { B where B is Affine Subset of (TOP-REAL n) : At c= B } implies x in Y )
assume Y in { B where B is Affine Subset of (TOP-REAL n) : At c= B } ; :: thesis: x in Y
then consider B being Affine Subset of (TOP-REAL n) such that
A7: ( Y = B & At c= B ) ;
reconsider A = B as Subset of (REAL-NS n) by Th4;
reconsider A = A as Affine Subset of (REAL-NS n) by Th40;
( Y = A & Ar c= A ) by A1, A7;
then Y in { B where B is Affine Subset of (REAL-NS n) : Ar c= B } ;
hence x in Y by A2, A6, SETFAM_1:def 1; :: thesis: verum
end;
hence x in Affin At by A4; :: thesis: verum
end;
assume A8: x in Affin At ; :: thesis: x in Affin Ar
now :: thesis: for Y being set st Y in { B where B is Affine Subset of (REAL-NS n) : Ar c= B } holds
x in Y
let Y be set ; :: thesis: ( Y in { B where B is Affine Subset of (REAL-NS n) : Ar c= B } implies x in Y )
assume Y in { B where B is Affine Subset of (REAL-NS n) : Ar c= B } ; :: thesis: x in Y
then consider B being Affine Subset of (REAL-NS n) such that
A9: ( Y = B & Ar c= B ) ;
reconsider A = B as Subset of (TOP-REAL n) by Th4;
reconsider A = A as Affine Subset of (TOP-REAL n) by Th40;
( Y = B & At c= A ) by A1, A9;
then Y in { B where B is Affine Subset of (TOP-REAL n) : At c= B } ;
hence x in Y by A3, A8, SETFAM_1:def 1; :: thesis: verum
end;
hence x in Affin Ar by A5; :: thesis: verum
end;
hence Affin Ar = Affin At by TARSKI:2; :: thesis: verum