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 B2 = { ((uparrow x) `) where x is Element of L2 : verum } ;
set B1 = { ((uparrow x) `) where x is Element of L1 : verum } ;
A2: { ((uparrow x) `) where x is Element of L1 : verum } is prebasis of L1 by Def1;
A3: { ((uparrow x) `) where x is Element of L2 : verum } is prebasis of L2 by Def1;
{ ((uparrow x) `) where x is Element of L1 : verum } = { ((uparrow x) `) where x is Element of L2 : verum } by A1, Lm1;
hence the topology of L1 = the topology of L2 by A1, A2, A3, YELLOW_9:26; :: thesis: verum