ex T being strict TopSpace st
( the carrier of T = F₁() & ( for A being Subset of T holds Int A = F₂(A) ) )

A1: F₂(F₁()) = F₁() and
A2: for A being Subset of F₁() holds F₂(A) c= A and
A3: for A, B being Subset of F₁() holds F₂((A /\ B)) = F₂(A) /\ F₂(B) and
A4: for A being Subset of F₁() holds F₂(F₂(A)) = F₂(A)