let X be non empty TopSpace; :: thesis: 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 )

let X1, X2, Y1, Y2 be non empty SubSpace of X; :: thesis: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition implies ( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 ) )

reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;

reconsider B1 = the carrier of Y1, B2 = the carrier of Y2 as Subset of X by TSEP_1:1;

assume that

A1: X1,Y1 constitute_a_decomposition and

A2: X2,Y2 constitute_a_decomposition ; :: thesis: ( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 )

A3: A2,B2 constitute_a_decomposition by A2;

then A4: A2 = B2 ` by Th3;

A5: A2 = B2 ` by A3, Th3;

A6: A1,B1 constitute_a_decomposition by A1;

then A7: A1 = B1 ` by Th3;

thus ( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) implies X1 misses X2 ) :: thesis: ( X1 misses X2 implies Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) )

then A1 misses A2 ;

then A8: A1 /\ A2 = {} X ;

A1 = B1 ` by A6, Th3;

then (B1 \/ B2) ` = {} X by A4, A8, XBOOLE_1:53;

then B1 \/ B2 = ({} X) ` ;

then A9: the carrier of (Y1 union Y2) = the carrier of X by TSEP_1:def 2;

X is SubSpace of X by TSEP_1:2;

hence Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) by A9, TSEP_1:5; :: thesis: verum

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

let X1, X2, Y1, Y2 be non empty SubSpace of X; :: thesis: ( X1,Y1 constitute_a_decomposition & X2,Y2 constitute_a_decomposition implies ( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 ) )

reconsider A1 = the carrier of X1, A2 = the carrier of X2 as Subset of X by TSEP_1:1;

reconsider B1 = the carrier of Y1, B2 = the carrier of Y2 as Subset of X by TSEP_1:1;

assume that

A1: X1,Y1 constitute_a_decomposition and

A2: X2,Y2 constitute_a_decomposition ; :: thesis: ( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) iff X1 misses X2 )

A3: A2,B2 constitute_a_decomposition by A2;

then A4: A2 = B2 ` by Th3;

A5: A2 = B2 ` by A3, Th3;

A6: A1,B1 constitute_a_decomposition by A1;

then A7: A1 = B1 ` by Th3;

thus ( Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) implies X1 misses X2 ) :: thesis: ( X1 misses X2 implies Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) )

proof

assume
X1 misses X2
; :: thesis: Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #)
assume
Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #)
; :: thesis: X1 misses X2

then B1 \/ B2 = the carrier of X by TSEP_1:def 2;

then (B1 \/ B2) ` = {} X by XBOOLE_1:37;

then A1 /\ A2 = {} by A7, A5, XBOOLE_1:53;

then A1 misses A2 ;

hence X1 misses X2 ; :: thesis: verum

end;then B1 \/ B2 = the carrier of X by TSEP_1:def 2;

then (B1 \/ B2) ` = {} X by XBOOLE_1:37;

then A1 /\ A2 = {} by A7, A5, XBOOLE_1:53;

then A1 misses A2 ;

hence X1 misses X2 ; :: thesis: verum

then A1 misses A2 ;

then A8: A1 /\ A2 = {} X ;

A1 = B1 ` by A6, Th3;

then (B1 \/ B2) ` = {} X by A4, A8, XBOOLE_1:53;

then B1 \/ B2 = ({} X) ` ;

then A9: the carrier of (Y1 union Y2) = the carrier of X by TSEP_1:def 2;

X is SubSpace of X by TSEP_1:2;

hence Y1 union Y2 = TopStruct(# the carrier of X, the topology of X #) by A9, TSEP_1:5; :: thesis: verum