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

proof

let A be Subset of X; :: thesis: H₁(A) c= A
( A = X or A <> X ) ;
then ( H₁(A) = A or H₁(A) = A /\ X0 ) by FUNCOP_1:def 8;
hence H₁(A) c= A by XBOOLE_1:17; :: thesis: verum

end;

A3: 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 = X or B = X or ( A <> X & B <> X ) ) ;

suppose A4: ( A = X or B = X ) ; :: thesis: H₁(A /\ B) = H₁(A) /\ H₁(B)

( ( A = X or A <> X ) & ( B = X or B <> X ) ) ;
then ( ( H₁(A) = A or H₁(A) = A /\ X0 ) & A /\ X0 c= A & B /\ X0 c= B & ( H₁(B) = B or H₁(B) = B /\ X0 ) ) by FUNCOP_1:def 8, XBOOLE_1:17;
then ( A /\ X = A & B /\ X = B & H₁(A) /\ X = H₁(A) & X /\ H₁(B) = H₁(B) ) by XBOOLE_1:28;
hence H₁(A /\ B) = H₁(A) /\ H₁(B) by A4, FUNCOP_1:def 8; :: thesis: verum

end;

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

A \/ (A /\ B) = A by XBOOLE_1:22;
then A /\ B <> X by A5, XBOOLE_1:12;
then A6: ( H₁(A) = A /\ X0 & H₁(B) = B /\ X0 & X0 = X0 /\ X0 & H₁(A /\ B) = (A /\ B) /\ X0 ) by A5, FUNCOP_1:def 8;
then H₁(A /\ B) = ((A /\ B) /\ X0) /\ X0 by XBOOLE_1:16;
then H₁(A /\ B) = ((B /\ X0) /\ A) /\ X0 by XBOOLE_1:16;
hence H₁(A /\ B) = H₁(A) /\ H₁(B) by A6, XBOOLE_1:16; :: thesis: verum

end;

end;

end;

A7: 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 = X or A <> X ) ;
then ( H₁(A) = X or ( A /\ X0 <> X & H₁(A) = A /\ X0 ) ) by FUNCOP_1:def 8;
then ( H₁(H₁(A)) = H₁(A) or ( H₁(A) = A /\ X0 & H₁(H₁(A)) = (A /\ X0) /\ X0 & X0 /\ X0 = X0 ) ) by FUNCOP_1:def 8;
hence H₁(H₁(A)) = H₁(A) by XBOOLE_1:16; :: thesis: verum

end;

consider T being strict TopSpace such that
A8: ( the carrier of T = X & ( for A being Subset of T holds Int A = H₁(A) ) ) from TOPGEN_3:sch 3(A1, A2, A3, A7);
take T ; :: thesis: ( the carrier of T = X & ( for A being Subset of T holds Int A = IFEQ A,X,A,(A /\ X0) ) )
thus the carrier of T = X by A8; :: thesis: for A being Subset of T holds Int A = IFEQ A,X,A,(A /\ X0)
let F be Subset of T; :: thesis: Int F = IFEQ F,X,F,(F /\ X0)
thus Int F = IFEQ F,X,F,(F /\ X0) by A8; :: thesis: verum