ex T being strict TopSpace st
( the carrier of T = F₁() & ( for A being Subset of T holds
( A is closed iff P₁[A] ) ) )

A1: ( P₁[ {} ] & P₁[F₁()] ) and
A2: for A, B being set st P₁[A] & P₁[B] holds
P₁[A \/ B] and
A3: for G being Subset-Family of F₁() st ( for A being set st A in G holds
P₁[A] ) holds
P₁[ Intersect G]