let T be non empty TopStruct ; :: thesis: for A, B being Subset of T holds (Cl_Seq A) \/ (Cl_Seq B) = Cl_Seq (A \/ B)
let A, B be Subset of T; :: thesis: (Cl_Seq A) \/ (Cl_Seq B) = Cl_Seq (A \/ B)
thus (Cl_Seq A) \/ (Cl_Seq B) c= Cl_Seq (A \/ B) :: according to XBOOLE_0:def 10 :: thesis: Cl_Seq (A \/ B) c= (Cl_Seq A) \/ (Cl_Seq B)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Cl_Seq A) \/ (Cl_Seq B) or x in Cl_Seq (A \/ B) )
assume A1: x in (Cl_Seq A) \/ (Cl_Seq B) ; :: thesis: x in Cl_Seq (A \/ B)

per cases ( x in Cl_Seq A or x in Cl_Seq B ) by A1, XBOOLE_0:def 3;

suppose A2: x in Cl_Seq A ; :: thesis: x in Cl_Seq (A \/ B)

then reconsider x9 = x as Point of T ;
consider S being sequence of T such that
A3: rng S c= A and
A4: x9 in Lim S by A2, Def1;
A c= A \/ B by XBOOLE_1:7;
then rng S c= A \/ B by A3;
hence x in Cl_Seq (A \/ B) by A4, Def1; :: thesis: verum

end;

suppose A5: x in Cl_Seq B ; :: thesis: x in Cl_Seq (A \/ B)

then reconsider x9 = x as Point of T ;
consider S being sequence of T such that
A6: rng S c= B and
A7: x9 in Lim S by A5, Def1;
B c= A \/ B by XBOOLE_1:7;
then rng S c= A \/ B by A6;
hence x in Cl_Seq (A \/ B) by A7, Def1; :: thesis: verum

end;

end;

end;

thus Cl_Seq (A \/ B) c= (Cl_Seq A) \/ (Cl_Seq B) :: thesis: verum

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Cl_Seq (A \/ B) or x in (Cl_Seq A) \/ (Cl_Seq B) )
assume A8: x in Cl_Seq (A \/ B) ; :: thesis: x in (Cl_Seq A) \/ (Cl_Seq B)
then reconsider x9 = x as Point of T ;
consider S being sequence of T such that
A9: rng S c= A \/ B and
A10: x9 in Lim S by A8, Def1;
consider S1 being subsequence of S such that
A11: ( rng S1 c= A or rng S1 c= B ) by A9, Th4;
A12: Lim S c= Lim S1 by Th16;

per cases ( rng S1 c= A or rng S1 c= B ) by A11;

suppose rng S1 c= A ; :: thesis: x in (Cl_Seq A) \/ (Cl_Seq B)

then x9 in Cl_Seq A by A10, A12, Def1;
hence x in (Cl_Seq A) \/ (Cl_Seq B) by XBOOLE_0:def 3; :: thesis: verum

end;

suppose rng S1 c= B ; :: thesis: x in (Cl_Seq A) \/ (Cl_Seq B)

then x9 in Cl_Seq B by A10, A12, Def1;
hence x in (Cl_Seq A) \/ (Cl_Seq B) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;