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)) #) ; :: thesis: ( 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; :: thesis: verum