set R = the Approximation_Space;
set C = the carrier of the Approximation_Space;
set I = the InternalRel of 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)) #)
; ( TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is naturally_generated & 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 )
T2:
( TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is with_equivalence & not TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is empty )
;
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)) #) #)
;
then
TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is naturally_generated
by Fiu;
hence
( TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is naturally_generated & 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 T2; verum