{ (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } c= bool ([#] T)

proof

hence
{ (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } is Subset-Family of ([#] T)
; :: thesis: verum
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } or t in bool ([#] T) )

assume t in { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } ; :: thesis: t in bool ([#] T)

then consider A0, B0 being Subset of T such that

A1: t = A0 /\ B0 and

A0 is open and

B0 is closed ;

reconsider t0 = t as set by A1;

( not [#] T is empty & A0 is Subset of ([#] T) & B0 is Subset of ([#] T) ) by STRUCT_0:def 3;

then t0 c= ([#] T) /\ ([#] T) by A1, XBOOLE_1:27;

hence t in bool ([#] T) ; :: thesis: verum

end;assume t in { (A /\ B) where A, B is Subset of T : ( A is open & B is closed ) } ; :: thesis: t in bool ([#] T)

then consider A0, B0 being Subset of T such that

A1: t = A0 /\ B0 and

A0 is open and

B0 is closed ;

reconsider t0 = t as set by A1;

( not [#] T is empty & A0 is Subset of ([#] T) & B0 is Subset of ([#] T) ) by STRUCT_0:def 3;

then t0 c= ([#] T) /\ ([#] T) by A1, XBOOLE_1:27;

hence t in bool ([#] T) ; :: thesis: verum