deffunc H_{1}( set ) -> set = IFEQ ($1,X,$1,($1 /\ X0));

A1: for A being Subset of X holds H_{1}(A) c= A
_{1}(A /\ B) = H_{1}(A) /\ H_{1}(B)
_{1}(H_{1}(A)) = H_{1}(A)
_{1}(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_{1}(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

A1: for A being Subset of X holds H

proof

A2:
for A, B being Subset of X holds H
let A be Subset of X; :: thesis: H_{1}(A) c= A

( A = X or A <> X ) ;

then ( H_{1}(A) = A or H_{1}(A) = A /\ X0 )
by FUNCOP_1:def 8;

hence H_{1}(A) c= A
by XBOOLE_1:17; :: thesis: verum

end;( A = X or A <> X ) ;

then ( H

hence H

proof

A11:
for A being Subset of X holds H
let A, B be Subset of X; :: thesis: H_{1}(A /\ B) = H_{1}(A) /\ H_{1}(B)

end;per cases
( A = X or B = X or ( A <> X & B <> X ) )
;

end;

suppose A3:
( A = X or B = X )
; :: thesis: H_{1}(A /\ B) = H_{1}(A) /\ H_{1}(B)

A4:
B /\ X = B
by XBOOLE_1:28;

( B = X or B <> X ) ;

then ( H_{1}(B) = B or H_{1}(B) = B /\ X0 )
by FUNCOP_1:def 8;

then A5: X /\ H_{1}(B) = H_{1}(B)
by XBOOLE_1:28;

( A = X or A <> X ) ;

then ( H_{1}(A) = A or H_{1}(A) = A /\ X0 )
by FUNCOP_1:def 8;

then A6: H_{1}(A) /\ X = H_{1}(A)
by XBOOLE_1:28;

A /\ X = A by XBOOLE_1:28;

hence H_{1}(A /\ B) = H_{1}(A) /\ H_{1}(B)
by A4, A6, A5, A3, FUNCOP_1:def 8; :: thesis: verum

end;( B = X or B <> X ) ;

then ( H

then A5: X /\ H

( A = X or A <> X ) ;

then ( H

then A6: H

A /\ X = A by XBOOLE_1:28;

hence H

suppose A7:
( A <> X & B <> X )
; :: thesis: H_{1}(A /\ B) = H_{1}(A) /\ H_{1}(B)

A \/ (A /\ B) = A
by XBOOLE_1:22;

then A /\ B <> X by A7, XBOOLE_1:12;

then A8: H_{1}(A /\ B) = (A /\ B) /\ X0
by FUNCOP_1:def 8;

X0 = X0 /\ X0 ;

then H_{1}(A /\ B) = ((A /\ B) /\ X0) /\ X0
by A8, XBOOLE_1:16;

then A9: H_{1}(A /\ B) = ((B /\ X0) /\ A) /\ X0
by XBOOLE_1:16;

A10: H_{1}(B) = B /\ X0
by A7, FUNCOP_1:def 8;

H_{1}(A) = A /\ X0
by A7, FUNCOP_1:def 8;

hence H_{1}(A /\ B) = H_{1}(A) /\ H_{1}(B)
by A9, A10, XBOOLE_1:16; :: thesis: verum

end;then A /\ B <> X by A7, XBOOLE_1:12;

then A8: H

X0 = X0 /\ X0 ;

then H

then A9: H

A10: H

H

hence H

proof

A12:
H
let A be Subset of X; :: thesis: H_{1}(H_{1}(A)) = H_{1}(A)

( A = X or A <> X ) ;

then ( H_{1}(A) = X or ( A /\ X0 <> X & H_{1}(A) = A /\ X0 ) )
by FUNCOP_1:def 8;

then ( H_{1}(H_{1}(A)) = H_{1}(A) or ( H_{1}(A) = A /\ X0 & H_{1}(H_{1}(A)) = (A /\ X0) /\ X0 & X0 /\ X0 = X0 ) )
by FUNCOP_1:def 8;

hence H_{1}(H_{1}(A)) = H_{1}(A)
by XBOOLE_1:16; :: thesis: verum

end;( A = X or A <> X ) ;

then ( H

then ( H

hence H

consider T being strict TopSpace such that

A13: ( the carrier of T = X & ( for A being Subset of T holds Int A = H

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