deffunc H1( set ) -> set = IFEQ ($1,{},$1,($1 \/ ({x0} /\ X)));
A1:
for A being Subset of X holds
( A c= H1(A) & H1(A) c= X )
A3:
H1( {} ) = {}
by FUNCOP_1:def 8;
A4:
for A, B being Subset of X holds H1(A \/ B) = H1(A) \/ H1(B)
A8:
for A being Subset of X holds H1(H1(A)) = H1(A)
consider T being strict TopSpace such that
A9:
( the carrier of T = X & ( for A being Subset of T holds Cl A = H1(A) ) )
from TOPGEN_3:sch 2(A3, A1, A4, A8);
take
T
; ( the carrier of T = X & ( for A being Subset of T holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X))) ) )
thus
the carrier of T = X
by A9; for A being Subset of T holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X)))
let F be Subset of T; Cl F = IFEQ (F,{},F,(F \/ ({x0} /\ X)))
thus
Cl F = IFEQ (F,{},F,(F \/ ({x0} /\ X)))
by A9; verum