set S = { <*x,t*> where x, t is Real : ( x in [#] REAL & t in [#] REAL ) } ;
for z being object holds
( z in [#] (REAL 2) iff z in { <*x,t*> where x, t is Real : ( x in [#] REAL & t in [#] REAL ) } )

proof

let z be object ; :: thesis: ( z in [#] (REAL 2) iff z in { <*x,t*> where x, t is Real : ( x in [#] REAL & t in [#] REAL ) } )

hereby :: thesis: ( z in { <*x,t*> where x, t is Real : ( x in [#] REAL & t in [#] REAL ) } implies z in [#] (REAL 2) )

assume z in [#] (REAL 2) ; :: thesis: z in { <*x,t*> where x, t is Real : ( x in [#] REAL & t in [#] REAL ) }
then z in { <*d1,d2*> where d1, d2 is Element of REAL : verum } by FINSEQ_2:99;
then ex d1, d2 being Element of REAL st z = <*d1,d2*> ;
hence z in { <*x,t*> where x, t is Real : ( x in [#] REAL & t in [#] REAL ) } ; :: thesis: verum

end;

assume z in { <*x,t*> where x, t is Real : ( x in [#] REAL & t in [#] REAL ) } ; :: thesis: z in [#] (REAL 2)
then ex x, t being Real st
( z = <*x,t*> & x in [#] REAL & t in [#] REAL ) ;
then z in { <*d1,d2*> where d1, d2 is Element of REAL : verum } ;
hence z in [#] (REAL 2) by FINSEQ_2:99; :: thesis: verum

end;

hence [#] (REAL 2) = { <*x,t*> where x, t is Real : ( x in [#] REAL & t in [#] REAL ) } by TARSKI:2; :: thesis: verum