let X be non empty TopSpace; for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 meets Y2 & Y1 meet Y2 = X1 meet X2 & X1,X2 are_weakly_separated holds
Y1,Y2 are_weakly_separated
let X1, X2, Y1, Y2 be non empty SubSpace of X; ( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 meets Y2 & Y1 meet Y2 = X1 meet X2 & X1,X2 are_weakly_separated implies Y1,Y2 are_weakly_separated )
reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
assume
( Y1 is SubSpace of X1 & Y2 is SubSpace of X2 )
; ( not Y1 meets Y2 or not Y1 meet Y2 = X1 meet X2 or not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
then A1:
( C1 c= A1 & C2 c= A2 )
by TSEP_1:4;
assume A2:
Y1 meets Y2
; ( not Y1 meet Y2 = X1 meet X2 or not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume A3:
Y1 meet Y2 = X1 meet X2
; ( not X1,X2 are_weakly_separated or Y1,Y2 are_weakly_separated )
assume
X1,X2 are_weakly_separated
; Y1,Y2 are_weakly_separated
then A4:
A1,A2 are_weakly_separated
;
now for C1, C2 being Subset of X st C1 = the carrier of Y1 & C2 = the carrier of Y2 holds
C1,C2 are_weakly_separated let C1,
C2 be
Subset of
X;
( C1 = the carrier of Y1 & C2 = the carrier of Y2 implies C1,C2 are_weakly_separated )assume A5:
(
C1 = the
carrier of
Y1 &
C2 = the
carrier of
Y2 )
;
C1,C2 are_weakly_separated then
C1 meets C2
by A2;
then
C1 /\ C2 <> {}
;
then
A1 /\ A2 <> {}
by A1, A5, XBOOLE_1:3, XBOOLE_1:27;
then
A1 meets A2
;
then
X1 meets X2
;
then
A1 /\ A2 = the
carrier of
(X1 meet X2)
by TSEP_1:def 4;
then
A1 /\ A2 = C1 /\ C2
by A2, A3, A5, TSEP_1:def 4;
hence
C1,
C2 are_weakly_separated
by A1, A4, A5, Th24;
verum end;
hence
Y1,Y2 are_weakly_separated
; verum