let TS be TopSpace; :: thesis: for P, Q being Subset of TS st P is boundary & Q is boundary & Q is closed holds
P \/ Q is boundary
let P, Q be Subset of TS; :: thesis: ( P is boundary & Q is boundary & Q is closed implies P \/ Q is boundary )
assume that
A1: P is boundary and
A2: Q is boundary and
A3: Q is closed ; :: thesis: P \/ Q is boundary
A4: Cl ((P `) \ Q) = Cl ((P `) /\ (Q `)) by SUBSET_1:13;
P ` is dense by A1;
then A5: ([#] TS) \ Q = (Cl (P `)) \ Q ;
A6: (Cl (P `)) \ (Cl Q) c= Cl ((P `) \ Q) by Th6;
Q ` is dense by A2;
then A7: Cl (Q `) = [#] TS ;
(Cl (P `)) \ Q = (Cl (P `)) \ (Cl Q) by A3, PRE_TOPC:22;
then ([#] TS) \ Q c= Cl ((P \/ Q) `) by A5, A6, A4, XBOOLE_1:53;
then Cl (Q `) c= Cl (Cl ((P \/ Q) `)) by PRE_TOPC:19;
then [#] TS = Cl ((P \/ Q) `) by A7;
then (P \/ Q) ` is dense ;
hence P \/ Q is boundary ; :: thesis: verum