deffunc H₁( set ) -> set = IFEQ ($1,{},$1,($1 \/ ({x0} /\ X)));
A1: 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 A2: ( 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 A2, XBOOLE_1:8; :: thesis: verum

end;

A3: H₁( {} ) = {} by FUNCOP_1:def 8;
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 A3; :: thesis: verum

end;

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

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

end;

end;

end;

A8: 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
A9: ( the carrier of T = X & ( for A being Subset of T holds Cl A = H₁(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