let L1, L2 be non empty TopSpace-like lower TopRelStr ; :: thesis: ( RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) implies the topology of L1 = the topology of L2 )
assume A1: RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) ; :: thesis: the topology of L1 = the topology of L2
set B1 = { ((uparrow x) ` ) where x is Element of L1 : verum } ;
set B2 = { ((uparrow x) ` ) where x is Element of L2 : verum } ;
A2: { ((uparrow x) ` ) where x is Element of L1 : verum } = { ((uparrow x) ` ) where x is Element of L2 : verum } by A1, Lm1;
( the carrier of L1 = the carrier of L2 & { ((uparrow x) ` ) where x is Element of L1 : verum } is prebasis of L1 & { ((uparrow x) ` ) where x is Element of L2 : verum } is prebasis of L2 ) by A1, Def1;
hence the topology of L1 = the topology of L2 by A2, YELLOW_9:26; :: thesis: verum