set R = the Approximation_Space;
set C = the carrier of the Approximation_Space;
set I = the InternalRel of the Approximation_Space;
set t = the Subset-Family of the carrier 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)) #);
T1: GenTop (LAp the Approximation_Space) is topology-like by ImportTop;
TopRelStr(# the carrier of the Approximation_Space, the InternalRel of the Approximation_Space,(GenTop (LAp the Approximation_Space)) #) is with_equivalence ;
hence ex b₁ being TopRelStr st
( b₁ is TopSpace-like & b₁ is with_equivalence & not b₁ is empty ) by T1; :: thesis: verum