let n be Element of NAT ; :: thesis: for B1, B2 being Subset of (TOP-REAL n)
for p being Point of (TOP-REAL n) st B1 c= B2 holds
B1 + p c= B2 + p
let B1, B2 be Subset of (TOP-REAL n); :: thesis: for p being Point of (TOP-REAL n) st B1 c= B2 holds
B1 + p c= B2 + p
let p be Point of (TOP-REAL n); :: thesis: ( B1 c= B2 implies B1 + p c= B2 + p )
assume A1: B1 c= B2 ; :: thesis: B1 + p c= B2 + p
let p1 be set ; :: according to TARSKI:def 3 :: thesis: ( not p1 in B1 + p or p1 in B2 + p )
assume p1 in B1 + p ; :: thesis: p1 in B2 + p
then consider p2 being Point of (TOP-REAL n) such that
A2: ( p1 = p2 + p & p2 in B1 ) ;
thus p1 in B2 + p by A1, A2; :: thesis: verum