deffunc H₁( set ) -> set = IFEQ $1,{} ,$1,($1 \/ ({x0} /\ X));
A1: H₁( {} ) = {} by FUNCOP_1:def 8;
A2: for A being Subset of X holds
( A c= H₁(A) & H₁(A) c= X )

proof

let A be Subset of X; :: thesis: ( A c= H₁(A) & H₁(A) c= X )
( A = {} or A <> {} ) ;
then A3: ( H₁(A) = A or H₁(A) = A \/ ({x0} /\ X) ) by FUNCOP_1:def 8;
hence A c= H₁(A) by XBOOLE_1:7; :: thesis: H₁(A) c= X
{x0} /\ X c= X by XBOOLE_1:17;
hence H₁(A) c= X by A3, XBOOLE_1:8; :: thesis: verum

end;

A4: for A, B being Subset of X holds H₁(A \/ B) = H₁(A) \/ H₁(B)

proof

let A, B be Subset of X; :: thesis: H₁(A \/ B) = H₁(A) \/ H₁(B)

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

suppose ( A = {} or B = {} ) ; :: thesis: H₁(A \/ B) = H₁(A) \/ H₁(B)

hence H₁(A \/ B) = H₁(A) \/ H₁(B) by A1; :: thesis: verum

end;

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

( H₁(A) = A \/ ({x0} /\ X) & H₁(B) = B \/ ({x0} /\ X) & H₁(A \/ B) = (A \/ B) \/ ({x0} /\ X) ) by A5, FUNCOP_1:def 8;
hence H₁(A \/ B) = H₁(A) \/ H₁(B) by XBOOLE_1:5; :: thesis: verum

end;

end;

end;

A6: for A being Subset of X holds H₁(H₁(A)) = H₁(A)

proof

let A be Subset of X; :: thesis: H₁(H₁(A)) = H₁(A)
( A = {} or A <> {} ) ;
then ( H₁(A) = {} or ( A \/ ({x0} /\ X) <> {} & H₁(A) = A \/ ({x0} /\ X) ) ) by FUNCOP_1:def 8;
then ( H₁(H₁(A)) = H₁(A) or ( H₁(A) = A \/ ({x0} /\ X) & H₁(H₁(A)) = (A \/ ({x0} /\ X)) \/ ({x0} /\ X) ) ) by FUNCOP_1:def 8;
hence H₁(H₁(A)) = H₁(A) by XBOOLE_1:6; :: thesis: verum

end;

consider T being strict TopSpace such that
A7: ( the carrier of T = X & ( for A being Subset of T holds Cl A = H₁(A) ) ) from TOPGEN_3:sch 2(A1, A2, A4, A6);
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 A7; :: 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 A7; :: thesis: verum