let X be non empty TopSpace; for X1, X2, Y1, Y2 being SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
let X1, X2, Y1, Y2 be SubSpace of X; ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_weakly_separated implies Y1,Y2 are_weakly_separated )
assume A1:
for A1, B1 being Subset of X st A1 = the carrier of X1 & B1 = the carrier of Y1 holds
A1,B1 constitute_a_decomposition
; TSEP_2:def 2 ( not X2,Y2 constitute_a_decomposition or not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume A2:
for A2, B2 being Subset of X st A2 = the carrier of X2 & B2 = the carrier of Y2 holds
A2,B2 constitute_a_decomposition
; TSEP_2:def 2 ( not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume A3:
for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated
; TSEP_1:def 7 Y1,Y2 are_weakly_separated
now for B1, B2 being Subset of X st B1 = the carrier of Y1 & B2 = the carrier of Y2 holds
B1,B2 are_weakly_separated reconsider A1 = the
carrier of
X1,
A2 = the
carrier of
X2 as
Subset of
X by TSEP_1:1;
let B1,
B2 be
Subset of
X;
( B1 = the carrier of Y1 & B2 = the carrier of Y2 implies B1,B2 are_weakly_separated )assume
(
B1 = the
carrier of
Y1 &
B2 = the
carrier of
Y2 )
;
B1,B2 are_weakly_separated then A4:
(
A1,
B1 constitute_a_decomposition &
A2,
B2 constitute_a_decomposition )
by A1, A2;
A1,
A2 are_weakly_separated
by A3;
hence
B1,
B2 are_weakly_separated
by A4, Th15;
verum end;
hence
Y1,Y2 are_weakly_separated
; verum