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 ` ))) )
thus Border A is regular_open :: thesis: ( Border A = (Int (Cl A)) \ (Cl (Int A)) & Border A = (Int (Cl A)) /\ (Int (Cl (A ` ))) )

proof

Fr A = Cl (Fr A) by PRE_TOPC:52;
hence Border A is regular_open ; :: thesis: verum

end;

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

proof

(Int (Cl A)) \ (Cl (Int A)) = (Int (Cl A)) \ (((Cl (Int A)) ` ) ` )
.= (Int (Cl A)) \ ((Int ((Int A) ` )) ` ) by TDLAT_3:4
.= (Int (Cl A)) \ ((Int (Cl (A ` ))) ` ) by TDLAT_3:3
.= (Int (Cl A)) /\ (((Int (Cl (A ` ))) ` ) ` ) by SUBSET_1:32
.= Int ((Cl A) /\ (Cl (A ` ))) by TOPS_1:46
.= Int (Fr A) by TOPS_1:def 2 ;
hence Border A = (Int (Cl A)) \ (Cl (Int A)) ; :: thesis: verum

end;

(Int (Cl A)) /\ (Int (Cl (A ` ))) = Int ((Cl A) /\ (Cl (A ` ))) by TOPS_1:46
.= Int (Fr A) by TOPS_1:def 2 ;
hence Border A = (Int (Cl A)) /\ (Int (Cl (A ` ))) ; :: thesis: verum