deffunc H₁( set ) -> set = IFEQ ($1,X,$1,($1 /\ X0));
A1: 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;

A2: 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 A3: ( A = X or B = X ) ; :: thesis: H₁(A /\ B) = H₁(A) /\ H₁(B)

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

end;

suppose A7: ( 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 A7, XBOOLE_1:12;
then A8: H₁(A /\ B) = (A /\ B) /\ X0 by FUNCOP_1:def 8;
X0 = X0 /\ X0 ;
then H₁(A /\ B) = ((A /\ B) /\ X0) /\ X0 by A8, XBOOLE_1:16;
then A9: H₁(A /\ B) = ((B /\ X0) /\ A) /\ X0 by XBOOLE_1:16;
A10: H₁(B) = B /\ X0 by A7, FUNCOP_1:def 8;
H₁(A) = A /\ X0 by A7, FUNCOP_1:def 8;
hence H₁(A /\ B) = H₁(A) /\ H₁(B) by A9, A10, XBOOLE_1:16; :: thesis: verum

end;

end;

end;

A11: 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;

A12: H₁(X) = X by FUNCOP_1:def 8;
consider T being strict TopSpace such that
A13: ( the carrier of T = X & ( for A being Subset of T holds Int A = H₁(A) ) ) from TOPGEN_3:sch 3(A12, A1, A2, A11);
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 A13; :: 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 A13; :: thesis: verum