let T be non empty TopSpace; :: thesis: ( T is Frechet implies for A, B being Subset of T holds
( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) & Cl_Seq (Cl_Seq A) = Cl_Seq A ) )
assume A1: T is Frechet ; :: thesis: for A, B being Subset of T holds
( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) & Cl_Seq (Cl_Seq A) = Cl_Seq A )
let A, B be Subset of T; :: thesis: ( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) & Cl_Seq (Cl_Seq A) = Cl_Seq A )
thus ( Cl_Seq ({} T) = {} & A c= Cl_Seq A & Cl_Seq (A \/ B) = (Cl_Seq A) \/ (Cl_Seq B) ) by Th17, Th18, Th19; :: thesis: Cl_Seq (Cl_Seq A) = Cl_Seq A
thus Cl_Seq (Cl_Seq A) = Cl_Seq (Cl A) by A1, Th20
.= Cl (Cl A) by A1, Th20
.= Cl_Seq A by A1, Th20 ; :: thesis: verum