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, Def4;
then A5: ([#] TS) \ Q = (Cl (P `)) \ Q by Def3;
A6: (Cl (P `)) \ (Cl Q) c= Cl ((P `) \ Q) by Th32;
Q ` is dense by A2, Def4;
then A7: Cl (Q `) = [#] TS by Def3;
(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, XBOOLE_0:def 10;
then (P \/ Q) ` is dense by Def3;
hence P \/ Q is boundary by Def4; :: thesis: verum