deffunc H1( set ) -> set = IFEQ ($1,X,$1,($1 /\ X0));
A1: for A being Subset of X holds H1(A) c= A
proof
let A be Subset of X; :: thesis: H1(A) c= A
( A = X or A <> X ) ;
then ( H1(A) = A or H1(A) = A /\ X0 ) by FUNCOP_1:def 8;
hence H1(A) c= A by XBOOLE_1:17; :: thesis: verum
end;
A2: for A, B being Subset of X holds H1(A /\ B) = H1(A) /\ H1(B)
proof
let A, B be Subset of X; :: thesis: H1(A /\ B) = H1(A) /\ H1(B)
per cases ( A = X or B = X or ( A <> X & B <> X ) ) ;
suppose A3: ( A = X or B = X ) ; :: thesis: H1(A /\ B) = H1(A) /\ H1(B)
A4: B /\ X = B by XBOOLE_1:28;
( B = X or B <> X ) ;
then ( H1(B) = B or H1(B) = B /\ X0 ) by FUNCOP_1:def 8;
then A5: X /\ H1(B) = H1(B) by XBOOLE_1:28;
( A = X or A <> X ) ;
then ( H1(A) = A or H1(A) = A /\ X0 ) by FUNCOP_1:def 8;
then A6: H1(A) /\ X = H1(A) by XBOOLE_1:28;
A /\ X = A by XBOOLE_1:28;
hence H1(A /\ B) = H1(A) /\ H1(B) by A4, A6, A5, A3, FUNCOP_1:def 8; :: thesis: verum
end;
suppose A7: ( A <> X & B <> X ) ; :: thesis: H1(A /\ B) = H1(A) /\ H1(B)
A \/ (A /\ B) = A by XBOOLE_1:22;
then A /\ B <> X by A7, XBOOLE_1:12;
then A8: H1(A /\ B) = (A /\ B) /\ X0 by FUNCOP_1:def 8;
X0 = X0 /\ X0 ;
then H1(A /\ B) = ((A /\ B) /\ X0) /\ X0 by A8, XBOOLE_1:16;
then A9: H1(A /\ B) = ((B /\ X0) /\ A) /\ X0 by XBOOLE_1:16;
A10: H1(B) = B /\ X0 by A7, FUNCOP_1:def 8;
H1(A) = A /\ X0 by A7, FUNCOP_1:def 8;
hence H1(A /\ B) = H1(A) /\ H1(B) by A9, A10, XBOOLE_1:16; :: thesis: verum
end;
end;
end;
A11: for A being Subset of X holds H1(H1(A)) = H1(A)
proof
let A be Subset of X; :: thesis: H1(H1(A)) = H1(A)
( A = X or A <> X ) ;
then ( H1(A) = X or ( A /\ X0 <> X & H1(A) = A /\ X0 ) ) by FUNCOP_1:def 8;
then ( H1(H1(A)) = H1(A) or ( H1(A) = A /\ X0 & H1(H1(A)) = (A /\ X0) /\ X0 & X0 /\ X0 = X0 ) ) by FUNCOP_1:def 8;
hence H1(H1(A)) = H1(A) by XBOOLE_1:16; :: thesis: verum
end;
A12: H1(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 = H1(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