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

( A is 1st_class iff Border A is empty )

let A be Subset of T; :: thesis: ( A is 1st_class iff Border A is empty )

A1: ( Border A is empty implies A is 1st_class )

( A is 1st_class iff Border A is empty )

let A be Subset of T; :: thesis: ( A is 1st_class iff Border A is empty )

A1: ( Border A is empty implies A is 1st_class )

proof

( A is 1st_class implies Border A is empty )
assume
Border A is empty
; :: thesis: A is 1st_class

then (Int (Cl A)) \ (Cl (Int A)) = {} by Th21;

then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37;

hence A is 1st_class ; :: thesis: verum

end;then (Int (Cl A)) \ (Cl (Int A)) = {} by Th21;

then Int (Cl A) c= Cl (Int A) by XBOOLE_1:37;

hence A is 1st_class ; :: thesis: verum

proof

hence
( A is 1st_class iff Border A is empty )
by A1; :: thesis: verum
assume
A is 1st_class
; :: thesis: Border A is empty

then Int (Cl A) c= Cl (Int A) ;

then (Int (Cl A)) \ (Cl (Int A)) = {} by XBOOLE_1:37;

hence Border A is empty by Th21; :: thesis: verum

end;then Int (Cl A) c= Cl (Int A) ;

then (Int (Cl A)) \ (Cl (Int A)) = {} by XBOOLE_1:37;

hence Border A is empty by Th21; :: thesis: verum