let T be non empty TopSpace; :: thesis: ( capOpCl T is with_empty_element & capOpCl T is cap-closed & capOpCl T is diff-finite-partition-closed )
set SR = { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } ;
the topology of T is cup-closed cap-closed with_empty_element Subset-Family of ([#] T)

proof

A1: the topology of T is with_empty_element by PRE_TOPC:1;
A2: the topology of T is cap-closed by PRE_TOPC:def 1;
the topology of T is cup-closed

proof

now :: thesis: for x, y being set st x in the topology of T & y in the topology of T holds
x \/ y in the topology of T

let x, y be set ; :: thesis: ( x in the topology of T & y in the topology of T implies x \/ y in the topology of T )
assume A3: ( x in the topology of T & y in the topology of T ) ; :: thesis: x \/ y in the topology of T
{x,y} c= bool the carrier of T

proof

let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {x,y} or t in bool the carrier of T )
assume t in {x,y} ; :: thesis: t in bool the carrier of T
then t in the topology of T by A3, TARSKI:def 2;
hence t in bool the carrier of T ; :: thesis: verum

end;

then reconsider xy = {x,y} as Subset-Family of T ;
xy c= the topology of T by A3, TARSKI:def 2;
then union xy in the topology of T by PRE_TOPC:def 1;
hence x \/ y in the topology of T by ZFMISC_1:75; :: thesis: verum

end;

hence the topology of T is cup-closed ; :: thesis: verum

end;

hence the topology of T is cup-closed cap-closed with_empty_element Subset-Family of ([#] T) by A1, A2, STRUCT_0:def 3; :: thesis: verum

end;

then reconsider XS = the topology of T as cup-closed cap-closed with_empty_element Subset-Family of ([#] T) ;
{ (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } = semidiff XS

proof

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: semidiff XS c= { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) }

let x be object ; :: thesis: ( x in { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } implies x in semidiff XS )
assume x in { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } ; :: thesis: x in semidiff XS
then consider A, B being Subset of T such that
A4: x = A /\ B and
A5: A is open and
A6: B is closed ;
A is Element of bool ([#] T) by STRUCT_0:def 3;
then A7: A \ ([#] T) is empty by XBOOLE_1:37;
A8: A \ (([#] T) \ B) = (A \ ([#] T)) \/ (A /\ B) by XBOOLE_1:52
.= A /\ B by A7 ;
reconsider A1 = A, CB1 = ([#] T) \ B as Element of XS by A5, A6, PRE_TOPC:def 2, PRE_TOPC:def 3;
x = A1 \ CB1 by A4, A8;
hence x in semidiff XS by SETFAM_1:def 6; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in semidiff XS or x in { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } )
assume x in semidiff XS ; :: thesis: x in { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) }
then consider A, B being Element of XS such that
A9: x = A \ B by LemX1;
( A in the topology of T & B in the topology of T ) ;
then reconsider A1 = A, B1 = B as Subset of T ;
A10: ( A1 \ ([#] T) is empty & ([#] T) /\ B1 = B1 ) by XBOOLE_1:37, XBOOLE_1:28;
A11: ( A1 is open & B1 is open ) by PRE_TOPC:def 2;
A12: ([#] T) \ (([#] T) \ B1) = ([#] T) /\ B1 by XBOOLE_1:48
.= B1 by XBOOLE_1:28 ;
then A13: ([#] T) \ B1 is closed by PRE_TOPC:def 2, PRE_TOPC:def 3;
A1 \ (([#] T) \ (([#] T) \ B1)) = (A1 \ ([#] T)) \/ (A1 /\ (([#] T) \ B1)) by XBOOLE_1:52
.= A1 /\ (([#] T) \ B1) by A10 ;
hence x in { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } by A9, A11, A12, A13; :: thesis: verum

end;

hence ( capOpCl T is with_empty_element & capOpCl T is cap-closed & capOpCl T is diff-finite-partition-closed ) ; :: thesis: verum