deffunc H_{1}( set ) -> set = IFEQ ($1,{},$1,($1 \/ ({x0} /\ X)));

A1: for A being Subset of X holds

( A c= H_{1}(A) & H_{1}(A) c= X )
_{1}( {} ) = {}
by FUNCOP_1:def 8;

A4: for A, B being Subset of X holds H_{1}(A \/ B) = H_{1}(A) \/ H_{1}(B)
_{1}(H_{1}(A)) = H_{1}(A)

A9: ( the carrier of T = X & ( for A being Subset of T holds Cl A = H_{1}(A) ) )
from TOPGEN_3:sch 2(A3, A1, A4, A8);

take T ; :: thesis: ( 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; :: thesis: for A being Subset of T holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X)))

let F be Subset of T; :: thesis: Cl F = IFEQ (F,{},F,(F \/ ({x0} /\ X)))

thus Cl F = IFEQ (F,{},F,(F \/ ({x0} /\ X))) by A9; :: thesis: verum

A1: for A being Subset of X holds

( A c= H

proof

A3:
H
let A be Subset of X; :: thesis: ( A c= H_{1}(A) & H_{1}(A) c= X )

( A = {} or A <> {} ) ;

then A2: ( H_{1}(A) = A or H_{1}(A) = A \/ ({x0} /\ X) )
by FUNCOP_1:def 8;

hence A c= H_{1}(A)
by XBOOLE_1:7; :: thesis: H_{1}(A) c= X

{x0} /\ X c= X by XBOOLE_1:17;

hence H_{1}(A) c= X
by A2, XBOOLE_1:8; :: thesis: verum

end;( A = {} or A <> {} ) ;

then A2: ( H

hence A c= H

{x0} /\ X c= X by XBOOLE_1:17;

hence H

A4: for A, B being Subset of X holds H

proof

A8:
for A being Subset of X holds H
let A, B be Subset of X; :: thesis: H_{1}(A \/ B) = H_{1}(A) \/ H_{1}(B)

end;per cases
( A = {} or B = {} or ( A <> {} & B <> {} ) )
;

end;

suppose A5:
( A <> {} & B <> {} )
; :: thesis: H_{1}(A \/ B) = H_{1}(A) \/ H_{1}(B)

then A6:
H_{1}(A \/ B) = (A \/ B) \/ ({x0} /\ X)
by FUNCOP_1:def 8;

A7: H_{1}(B) = B \/ ({x0} /\ X)
by A5, FUNCOP_1:def 8;

H_{1}(A) = A \/ ({x0} /\ X)
by A5, FUNCOP_1:def 8;

hence H_{1}(A \/ B) = H_{1}(A) \/ H_{1}(B)
by A7, A6, XBOOLE_1:5; :: thesis: verum

end;A7: H

H

hence H

proof

consider T being strict TopSpace such that
let A be Subset of X; :: thesis: H_{1}(H_{1}(A)) = H_{1}(A)

( A = {} or A <> {} ) ;

then ( H_{1}(A) = {} or ( A \/ ({x0} /\ X) <> {} & H_{1}(A) = A \/ ({x0} /\ X) ) )
by FUNCOP_1:def 8;

then ( H_{1}(H_{1}(A)) = H_{1}(A) or ( H_{1}(A) = A \/ ({x0} /\ X) & H_{1}(H_{1}(A)) = (A \/ ({x0} /\ X)) \/ ({x0} /\ X) ) )
by FUNCOP_1:def 8;

hence H_{1}(H_{1}(A)) = H_{1}(A)
by XBOOLE_1:6; :: thesis: verum

end;( A = {} or A <> {} ) ;

then ( H

then ( H

hence H

A9: ( the carrier of T = X & ( for A being Subset of T holds Cl A = H

take T ; :: thesis: ( 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; :: thesis: for A being Subset of T holds Cl A = IFEQ (A,{},A,(A \/ ({x0} /\ X)))

let F be Subset of T; :: thesis: Cl F = IFEQ (F,{},F,(F \/ ({x0} /\ X)))

thus Cl F = IFEQ (F,{},F,(F \/ ({x0} /\ X))) by A9; :: thesis: verum