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