let t be Real; :: thesis: for n being Element of NAT
for X, Y being Subset of (TOP-REAL n) st X c= Y holds
t (.) X c= t (.) Y
let n be Element of NAT ; :: thesis: for X, Y being Subset of (TOP-REAL n) st X c= Y holds
t (.) X c= t (.) Y
let X, Y be Subset of (TOP-REAL n); :: thesis: ( X c= Y implies t (.) X c= t (.) Y )
assume A1: X c= Y ; :: thesis: t (.) X c= t (.) Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in t (.) X or x in t (.) Y )
assume x in t (.) X ; :: thesis: x in t (.) Y
then ex a being Point of (TOP-REAL n) st
( x = t * a & a in X ) ;
hence x in t (.) Y by A1; :: thesis: verum