theorem PiBase.Homeomorph.fullyT4Space {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] [FullyT4Space X] (f : X ≃ₜ Y) : FullyT4Space Y

theorem PiBase.WellDefined.fullyT4Space : WellDefined FullyT4Space