:: by Zbigniew Karno

::

:: Received November 9, 1992

:: Copyright (c) 1992-2021 Association of Mizar Users

:: Complemented Subsets.

definition

let X be 1-sorted ;

let A1, A2 be Subset of X;

for A1, A2 being Subset of X st A1 misses A2 & A1 \/ A2 = the carrier of X holds

( A2 misses A1 & A2 \/ A1 = the carrier of X ) ;

end;
let A1, A2 be Subset of X;

pred A1,A2 constitute_a_decomposition means :: TSEP_2:def 1

( A1 misses A2 & A1 \/ A2 = the carrier of X );

symmetry ( A1 misses A2 & A1 \/ A2 = the carrier of X );

for A1, A2 being Subset of X st A1 misses A2 & A1 \/ A2 = the carrier of X holds

( A2 misses A1 & A2 \/ A1 = the carrier of X ) ;

:: deftheorem defines constitute_a_decomposition TSEP_2:def 1 :

for X being 1-sorted

for A1, A2 being Subset of X holds

( A1,A2 constitute_a_decomposition iff ( A1 misses A2 & A1 \/ A2 = the carrier of X ) );

for X being 1-sorted

for A1, A2 being Subset of X holds

( A1,A2 constitute_a_decomposition iff ( A1 misses A2 & A1 \/ A2 = the carrier of X ) );

notation

let X be 1-sorted ;

let A1, A2 be Subset of X;

antonym A1,A2 do_not_constitute_a_decomposition for A1,A2 constitute_a_decomposition ;

end;
let A1, A2 be Subset of X;

antonym A1,A2 do_not_constitute_a_decomposition for A1,A2 constitute_a_decomposition ;

theorem :: TSEP_2:2

theorem Th3: :: TSEP_2:3

for X being non empty 1-sorted

for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds

( A1 = A2 ` & A2 = A1 ` )

for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds

( A1 = A2 ` & A2 = A1 ` )

proof end;

theorem Th4: :: TSEP_2:4

for X being non empty 1-sorted

for A1, A2 being Subset of X st ( A1 = A2 ` or A2 = A1 ` ) holds

A1,A2 constitute_a_decomposition

for A1, A2 being Subset of X st ( A1 = A2 ` or A2 = A1 ` ) holds

A1,A2 constitute_a_decomposition

proof end;

definition

let X be non empty 1-sorted ;

let A1, A2 be Subset of X;

:: original: constitute_a_decomposition

redefine pred A1,A2 constitute_a_decomposition ;

irreflexivity

for A1 being Subset of X holds (X,b_{1},b_{1})
by Th7;

end;
let A1, A2 be Subset of X;

:: original: constitute_a_decomposition

redefine pred A1,A2 constitute_a_decomposition ;

irreflexivity

for A1 being Subset of X holds (X,b

theorem Th8: :: TSEP_2:8

for X being non empty 1-sorted

for A, A1, A2 being Subset of X st A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition holds

A1 = A2

for A, A1, A2 being Subset of X st A1,A constitute_a_decomposition & A,A2 constitute_a_decomposition holds

A1 = A2

proof end;

theorem Th9: :: TSEP_2:9

for X being non empty TopSpace

for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds

( Cl A1, Int A2 constitute_a_decomposition & Int A1, Cl A2 constitute_a_decomposition )

for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds

( Cl A1, Int A2 constitute_a_decomposition & Int A1, Cl A2 constitute_a_decomposition )

proof end;

theorem :: TSEP_2:10

for X being non empty TopSpace

for A being Subset of X holds

( Cl A, Int (A `) constitute_a_decomposition & Cl (A `), Int A constitute_a_decomposition & Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )

for A being Subset of X holds

( Cl A, Int (A `) constitute_a_decomposition & Cl (A `), Int A constitute_a_decomposition & Int A, Cl (A `) constitute_a_decomposition & Int (A `), Cl A constitute_a_decomposition )

proof end;

theorem Th11: :: TSEP_2:11

for X being non empty TopSpace

for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds

( A1 is open iff A2 is closed )

for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds

( A1 is open iff A2 is closed )

proof end;

theorem :: TSEP_2:12

theorem Th13: :: TSEP_2:13

for X being non empty 1-sorted

for A1, A2, B1, B2 being Subset of X st A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition holds

A1 /\ B1,A2 \/ B2 constitute_a_decomposition

for A1, A2, B1, B2 being Subset of X st A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition holds

A1 /\ B1,A2 \/ B2 constitute_a_decomposition

proof end;

theorem :: TSEP_2:14

for X being non empty 1-sorted

for A1, A2, B1, B2 being Subset of X st A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition holds

A1 \/ B1,A2 /\ B2 constitute_a_decomposition by Th13;

for A1, A2, B1, B2 being Subset of X st A1,A2 constitute_a_decomposition & B1,B2 constitute_a_decomposition holds

A1 \/ B1,A2 /\ B2 constitute_a_decomposition by Th13;

theorem Th15: :: TSEP_2:15

for X being non empty TopSpace

for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition holds

( A1,A2 are_weakly_separated iff C1,C2 are_weakly_separated )

for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition holds

( A1,A2 are_weakly_separated iff C1,C2 are_weakly_separated )

proof end;

theorem :: TSEP_2:16

for X being non empty TopSpace

for A1, A2 being Subset of X holds

( A1,A2 are_weakly_separated iff A1 ` ,A2 ` are_weakly_separated )

for A1, A2 being Subset of X holds

( A1,A2 are_weakly_separated iff A1 ` ,A2 ` are_weakly_separated )

proof end;

theorem :: TSEP_2:17

for X being non empty TopSpace

for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1,A2 are_separated holds

C1,C2 are_weakly_separated

for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1,A2 are_separated holds

C1,C2 are_weakly_separated

proof end;

theorem Th18: :: TSEP_2:18

for X being non empty TopSpace

for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1 misses A2 & C1,C2 are_weakly_separated holds

A1,A2 are_separated

for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & A1 misses A2 & C1,C2 are_weakly_separated holds

A1,A2 are_separated

proof end;

theorem :: TSEP_2:19

for X being non empty TopSpace

for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & C1 \/ C2 = the carrier of X & C1,C2 are_weakly_separated holds

A1,A2 are_separated

for A1, A2, C1, C2 being Subset of X st A1,C1 constitute_a_decomposition & A2,C2 constitute_a_decomposition & C1 \/ C2 = the carrier of X & C1,C2 are_weakly_separated holds

A1,A2 are_separated

proof end;

theorem :: TSEP_2:20

for X being non empty TopSpace

for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds

( A1,A2 are_weakly_separated iff A1,A2 are_separated ) by TSEP_1:46;

for A1, A2 being Subset of X st A1,A2 constitute_a_decomposition holds

( A1,A2 are_weakly_separated iff A1,A2 are_separated ) by TSEP_1:46;

theorem Th21: :: TSEP_2:21

for X being non empty TopSpace

for A1, A2 being Subset of X holds

( A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated )

for A1, A2 being Subset of X holds

( A1,A2 are_weakly_separated iff (A1 \/ A2) \ A1,(A1 \/ A2) \ A2 are_separated )

proof end;

::An Enlargement Theorem for Subsets.

theorem Th22: :: TSEP_2:22

for X being non empty TopSpace

for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 \/ C2 = A1 \/ A2 & C1,C2 are_weakly_separated holds

A1,A2 are_weakly_separated

for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 \/ C2 = A1 \/ A2 & C1,C2 are_weakly_separated holds

A1,A2 are_weakly_separated

proof end;

theorem Th23: :: TSEP_2:23

for X being non empty TopSpace

for A1, A2 being Subset of X holds

( A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated )

for A1, A2 being Subset of X holds

( A1,A2 are_weakly_separated iff A1 \ (A1 /\ A2),A2 \ (A1 /\ A2) are_separated )

proof end;

::An Extenuation Theorem for Subsets.

theorem Th24: :: TSEP_2:24

for X being non empty TopSpace

for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 /\ C2 = A1 /\ A2 & A1,A2 are_weakly_separated holds

C1,C2 are_weakly_separated

for A1, A2, C1, C2 being Subset of X st C1 c= A1 & C2 c= A2 & C1 /\ C2 = A1 /\ A2 & A1,A2 are_weakly_separated holds

C1,C2 are_weakly_separated

proof end;

theorem Th25: :: TSEP_2:25

for X being non empty TopSpace

for A1, A2 being Subset of X

for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds

( A1,A2 are_separated iff B1,B2 are_separated )

for A1, A2 being Subset of X

for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = A1 & B2 = A2 holds

( A1,A2 are_separated iff B1,B2 are_separated )

proof end;

theorem Th26: :: TSEP_2:26

for X being non empty TopSpace

for A1, A2 being Subset of X

for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_separated holds

B1,B2 are_separated

for A1, A2 being Subset of X

for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_separated holds

B1,B2 are_separated

proof end;

theorem Th28: :: TSEP_2:28

for X being non empty TopSpace

for A1, A2 being Subset of X

for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds

B1,B2 are_weakly_separated

for A1, A2 being Subset of X

for X0 being non empty SubSpace of X

for B1, B2 being Subset of X0 st B1 = the carrier of X0 /\ A1 & B2 = the carrier of X0 /\ A2 & A1,A2 are_weakly_separated holds

B1,B2 are_weakly_separated

proof end;

:: 3. Certain Subspace-Decompositions of a Topological Space.

definition

let X be non empty TopSpace;

let X1, X2 be SubSpace of X;

for X1, X2 being SubSpace of X st ( for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds

A1,A2 constitute_a_decomposition ) holds

for A1, A2 being Subset of X st A1 = the carrier of X2 & A2 = the carrier of X1 holds

A1,A2 constitute_a_decomposition ;

end;
let X1, X2 be SubSpace of X;

pred X1,X2 constitute_a_decomposition means :: TSEP_2:def 2

for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds

A1,A2 constitute_a_decomposition ;

symmetry for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds

A1,A2 constitute_a_decomposition ;

for X1, X2 being SubSpace of X st ( for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds

A1,A2 constitute_a_decomposition ) holds

for A1, A2 being Subset of X st A1 = the carrier of X2 & A2 = the carrier of X1 holds

A1,A2 constitute_a_decomposition ;

:: deftheorem defines constitute_a_decomposition TSEP_2:def 2 :

for X being non empty TopSpace

for X1, X2 being SubSpace of X holds

( X1,X2 constitute_a_decomposition iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds

A1,A2 constitute_a_decomposition );

for X being non empty TopSpace

for X1, X2 being SubSpace of X holds

( X1,X2 constitute_a_decomposition iff for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds

A1,A2 constitute_a_decomposition );

notation

let X be non empty TopSpace;

let X1, X2 be SubSpace of X;

antonym X1,X2 do_not_constitute_a_decomposition for X1,X2 constitute_a_decomposition ;

end;
let X1, X2 be SubSpace of X;

antonym X1,X2 do_not_constitute_a_decomposition for X1,X2 constitute_a_decomposition ;

theorem Th29: :: TSEP_2:29

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X holds

( X1,X2 constitute_a_decomposition iff ( X1 misses X2 & TopStruct(# the carrier of X, the topology of X #) = X1 union X2 ) )

for X1, X2 being non empty SubSpace of X holds

( X1,X2 constitute_a_decomposition iff ( X1 misses X2 & TopStruct(# the carrier of X, the topology of X #) = X1 union X2 ) )

proof end;

theorem Th30: :: TSEP_2:30

for X being non empty TopSpace

for X0 being non empty SubSpace of X holds X0,X0 do_not_constitute_a_decomposition

for X0 being non empty SubSpace of X holds X0,X0 do_not_constitute_a_decomposition

proof end;

definition

let X be non empty TopSpace;

let A1, A2 be non empty SubSpace of X;

:: original: constitute_a_decomposition

redefine pred A1,A2 constitute_a_decomposition ;

irreflexivity

for A1 being non empty SubSpace of X holds (X,b_{1},b_{1})
by Th30;

end;
let A1, A2 be non empty SubSpace of X;

:: original: constitute_a_decomposition

redefine pred A1,A2 constitute_a_decomposition ;

irreflexivity

for A1 being non empty SubSpace of X holds (X,b

theorem :: TSEP_2:31

for X being non empty TopSpace

for X0, X1, X2 being non empty SubSpace of X st X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition holds

TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

for X0, X1, X2 being non empty SubSpace of X st X1,X0 constitute_a_decomposition & X0,X2 constitute_a_decomposition holds

TopStruct(# the carrier of X1, the topology of X1 #) = TopStruct(# the carrier of X2, the topology of X2 #)

proof end;

theorem Th32: :: TSEP_2:32

for X being non empty TopSpace

for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds

( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 )

for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition holds

( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 )

proof end;

theorem Th33: :: TSEP_2:33

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds

( X1 is open iff X2 is closed )

for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds

( X1 is open iff X2 is closed )

proof end;

theorem :: TSEP_2:34

theorem Th35: :: TSEP_2:35

for X being non empty TopSpace

for X1, X2, Y1, Y2 being non empty SubSpace of X st X1 meets Y1 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition holds

X1 meet Y1,X2 union Y2 constitute_a_decomposition

for X1, X2, Y1, Y2 being non empty SubSpace of X st X1 meets Y1 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition holds

X1 meet Y1,X2 union Y2 constitute_a_decomposition

proof end;

theorem :: TSEP_2:36

for X being non empty TopSpace

for X1, X2, Y1, Y2 being non empty SubSpace of X st X2 meets Y2 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition holds

X1 union Y1,X2 meet Y2 constitute_a_decomposition by Th35;

for X1, X2, Y1, Y2 being non empty SubSpace of X st X2 meets Y2 & X1,X2 constitute_a_decomposition & Y1,Y2 constitute_a_decomposition holds

X1 union Y1,X2 meet Y2 constitute_a_decomposition by Th35;

theorem Th37: :: TSEP_2:37

for X being 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

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

proof end;

theorem :: TSEP_2:38

for X being non empty TopSpace

for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_separated holds

Y1,Y2 are_weakly_separated by TSEP_1:78, Th37;

for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1,X2 are_separated holds

Y1,Y2 are_weakly_separated by TSEP_1:78, Th37;

theorem Th39: :: TSEP_2:39

for X being non empty TopSpace

for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1 misses X2 & Y1,Y2 are_weakly_separated holds

X1,X2 are_separated by Th37, TSEP_1:78;

for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & X1 misses X2 & Y1,Y2 are_weakly_separated holds

X1,X2 are_separated by Th37, TSEP_1:78;

theorem :: TSEP_2:40

for X being non empty TopSpace

for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) & Y1,Y2 are_weakly_separated holds

X1,X2 are_separated

for X1, X2, Y1, Y2 being non empty SubSpace of X st X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition & Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) & Y1,Y2 are_weakly_separated holds

X1,X2 are_separated

proof end;

theorem :: TSEP_2:41

for X being non empty TopSpace

for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds

( X1,X2 are_weakly_separated iff X1,X2 are_separated ) by Th29, TSEP_1:78;

for X1, X2 being non empty SubSpace of X st X1,X2 constitute_a_decomposition holds

( X1,X2 are_weakly_separated iff X1,X2 are_separated ) by Th29, TSEP_1:78;

::An Enlargement Theorem for Subspaces.

theorem :: TSEP_2:42

for X being 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 union Y2 = X1 union X2 & Y1,Y2 are_weakly_separated holds

X1,X2 are_weakly_separated

for X1, X2, Y1, Y2 being non empty SubSpace of X st Y1 is SubSpace of X1 & Y2 is SubSpace of X2 & Y1 union Y2 = X1 union X2 & Y1,Y2 are_weakly_separated holds

X1,X2 are_weakly_separated

proof end;

::An Extenuation Theorem for Subspaces.

theorem :: TSEP_2:43

for X being 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

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

proof end;

theorem Th44: :: TSEP_2:44

for X being non empty TopSpace

for X0 being non empty SubSpace of X

for X1, X2 being SubSpace of X

for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds

( X1,X2 are_separated iff Y1,Y2 are_separated )

for X0 being non empty SubSpace of X

for X1, X2 being SubSpace of X

for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds

( X1,X2 are_separated iff Y1,Y2 are_separated )

proof end;

theorem :: TSEP_2:45

for X being non empty TopSpace

for X0, X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds

for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_separated holds

Y1,Y2 are_separated

for X0, X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds

for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_separated holds

Y1,Y2 are_separated

proof end;

theorem :: TSEP_2:46

for X being non empty TopSpace

for X0 being non empty SubSpace of X

for X1, X2 being SubSpace of X

for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds

( X1,X2 are_weakly_separated iff Y1,Y2 are_weakly_separated )

for X0 being non empty SubSpace of X

for X1, X2 being SubSpace of X

for Y1, Y2 being SubSpace of X0 st the carrier of X1 = the carrier of Y1 & the carrier of X2 = the carrier of Y2 holds

( X1,X2 are_weakly_separated iff Y1,Y2 are_weakly_separated )

proof end;

theorem :: TSEP_2:47

for X being non empty TopSpace

for X0, X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds

for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_weakly_separated holds

Y1,Y2 are_weakly_separated

for X0, X1, X2 being non empty SubSpace of X st X1 meets X0 & X2 meets X0 holds

for Y1, Y2 being SubSpace of X0 st Y1 = X1 meet X0 & Y2 = X2 meet X0 & X1,X2 are_weakly_separated holds

Y1,Y2 are_weakly_separated

proof end;