set R = the Approximation_Space;
set C = the carrier of the Approximation_Space;
set I = the InternalRel of the Approximation_Space;
set f = LAp the Approximation_Space;
set F = GenTop (LAp the Approximation_Space);
set EX = TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #);
take TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) ; :: thesis: ( TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is Natural & TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is TopSpace-like & TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is with_equivalence )
t1: GenTop (LAp the Approximation_Space) is topology-like by ImportTop;
set T = TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #);
set U = RelStr(# the carrier of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #), the InternalRel of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) #);
XX: RelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space #) = RelStr(# the carrier of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #), the InternalRel of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) #) ;
for x being Subset of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) holds
( x in the topology of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) iff x is LAp TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) -closed )
proof
let x be Subset of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #); :: thesis: ( x in the topology of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) iff x is LAp TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) -closed )
hereby :: thesis: ( x is LAp TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) -closed implies x in the topology of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) )
assume x in the topology of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) ; :: thesis: x is LAp TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) -closed
then ex S being Subset of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) st
( S = x & S is LAp the Approximation_Space -closed ) by GTDef;
hence x is LAp TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) -closed by Fiu, XX; :: thesis: verum
end;
assume v4: x is LAp TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) -closed ; :: thesis: x in the topology of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #)
reconsider y = x as Subset of the Approximation_Space ;
y is LAp the Approximation_Space -closed by v4, Fiu, XX;
hence x in the topology of TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) by GTDef; :: thesis: verum
end;
hence ( TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is Natural & TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is TopSpace-like & TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is with_equivalence ) by t1; :: thesis: verum