let T be TopSpace; :: thesis: for A being Subset of T holds the carrier of T = ((Int A) \/ (Fr A)) \/ (Int (A ` ))
let A be Subset of T; :: thesis: the carrier of T = ((Int A) \/ (Fr A)) \/ (Int (A ` ))
((Int A) \/ (Fr A)) \/ (Int (A ` )) = ((Int A) \/ (Int (A ` ))) \/ (Fr A) by XBOOLE_1:4
.= ((Int A) \/ (Int (A ` ))) \/ ((Cl A) /\ (Cl (A ` ))) by TOPS_1:def 2
.= (((Int A) \/ (Int (A ` ))) \/ (Cl A)) /\ (((Int A) \/ (Int (A ` ))) \/ (Cl (A ` ))) by XBOOLE_1:24
.= (((Int A) \/ ((Cl A) ` )) \/ (Cl A)) /\ (((Int A) \/ (Int (A ` ))) \/ (Cl (A ` ))) by TDLAT_3:4
.= ((Int A) \/ (((Cl A) ` ) \/ (Cl A))) /\ (((Int A) \/ (Int (A ` ))) \/ (Cl (A ` ))) by XBOOLE_1:4
.= ((Int A) \/ ([#] T)) /\ (((Int A) \/ (Int (A ` ))) \/ (Cl (A ` ))) by PRE_TOPC:18
.= ((Int A) \/ ([#] T)) /\ (((Int A) \/ (Int (A ` ))) \/ ((Int A) ` )) by TDLAT_3:3
.= ((Int A) \/ ([#] T)) /\ (((Int A) \/ ((Int A) ` )) \/ (Int (A ` ))) by XBOOLE_1:4
.= ((Int A) \/ ([#] T)) /\ (([#] T) \/ (Int (A ` ))) by PRE_TOPC:18
.= ([#] T) /\ (([#] T) \/ (Int (A ` ))) by XBOOLE_1:12
.= ([#] T) /\ ([#] T) by XBOOLE_1:12
.= [#] T ;
hence the carrier of T = ((Int A) \/ (Fr A)) \/ (Int (A ` )) ; :: thesis: verum