let T be TopSpace; :: thesis: for A being Subset of T holds

( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )

let A be Subset of T; :: thesis: ( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )

Fr A = Cl (Fr A) by PRE_TOPC:22;

hence Border A is regular_open ; :: thesis: ( Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )

(Int (Cl A)) \ (Cl (Int A)) = (Int (Cl A)) \ (((Cl (Int A)) `) `)

.= (Int (Cl A)) \ ((Int ((Int A) `)) `) by TDLAT_3:3

.= (Int (Cl A)) \ ((Int (Cl (A `))) `) by TDLAT_3:2

.= (Int (Cl A)) /\ (((Int (Cl (A `))) `) `) by SUBSET_1:13

.= Int ((Cl A) /\ (Cl (A `))) by TOPS_1:17

.= Int (Fr A) by TOPS_1:def 2 ;

hence Border A = (Int (Cl A)) \ (Cl (Int A)) ; :: thesis: Border A = (Int (Cl A)) /\ (Int (Cl (A `)))

(Int (Cl A)) /\ (Int (Cl (A `))) = Int ((Cl A) /\ (Cl (A `))) by TOPS_1:17

.= Int (Fr A) by TOPS_1:def 2 ;

hence Border A = (Int (Cl A)) /\ (Int (Cl (A `))) ; :: thesis: verum

( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )

let A be Subset of T; :: thesis: ( Border A is regular_open & Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )

Fr A = Cl (Fr A) by PRE_TOPC:22;

hence Border A is regular_open ; :: thesis: ( Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A `))) )

(Int (Cl A)) \ (Cl (Int A)) = (Int (Cl A)) \ (((Cl (Int A)) `) `)

.= (Int (Cl A)) \ ((Int ((Int A) `)) `) by TDLAT_3:3

.= (Int (Cl A)) \ ((Int (Cl (A `))) `) by TDLAT_3:2

.= (Int (Cl A)) /\ (((Int (Cl (A `))) `) `) by SUBSET_1:13

.= Int ((Cl A) /\ (Cl (A `))) by TOPS_1:17

.= Int (Fr A) by TOPS_1:def 2 ;

hence Border A = (Int (Cl A)) \ (Cl (Int A)) ; :: thesis: Border A = (Int (Cl A)) /\ (Int (Cl (A `)))

(Int (Cl A)) /\ (Int (Cl (A `))) = Int ((Cl A) /\ (Cl (A `))) by TOPS_1:17

.= Int (Fr A) by TOPS_1:def 2 ;

hence Border A = (Int (Cl A)) /\ (Int (Cl (A `))) ; :: thesis: verum