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:3
.= ((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:2
.= ((Int A) \/ ([#] T)) /\ (((Int A) \/ (Int (A `))) \/ ((Int A) `)) by TDLAT_3:2
.= ((Int A) \/ ([#] T)) /\ (((Int A) \/ ((Int A) `)) \/ (Int (A `))) by XBOOLE_1:4
.= ((Int A) \/ ([#] T)) /\ (([#] T) \/ (Int (A `))) by PRE_TOPC:2
.= ([#] 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