let X be non empty TopSpace; for X0, X1, X2, Y1, Y2 being non empty SubSpace of X st X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & X0 meet (X1 union X2) is SubSpace of X1 meet X2 holds
( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
let X0, X1, X2, Y1, Y2 be non empty SubSpace of X; ( X1 meets X2 & X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & X0 meet (X1 union X2) is SubSpace of X1 meet X2 implies ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A1:
X1 meets X2
; ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or not TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 or not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or not X0 meet (X1 union X2) is SubSpace of X1 meet X2 or ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
reconsider C = the carrier of X0 as Subset of X by TSEP_1:1;
reconsider C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
reconsider C1 = the carrier of Y1 as Subset of X by TSEP_1:1;
reconsider A2 = the carrier of X2 as Subset of X by TSEP_1:1;
reconsider A1 = the carrier of X1 as Subset of X by TSEP_1:1;
assume that
A2:
X1 is not SubSpace of X2
and
A3:
X2 is not SubSpace of X1
; ( not TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0 or not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or not X0 meet (X1 union X2) is SubSpace of X1 meet X2 or ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A4:
TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union X0
; ( not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or not X0 meet (X1 union X2) is SubSpace of X1 meet X2 or ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume that
A5:
Y1 meet (X1 union X2) is SubSpace of X1
and
A6:
Y2 meet (X1 union X2) is SubSpace of X2
; ( not X0 meet (X1 union X2) is SubSpace of X1 meet X2 or ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume A7:
X0 meet (X1 union X2) is SubSpace of X1 meet X2
; ( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
A8:
the carrier of (X1 union X2) = A1 \/ A2
by TSEP_1:def 2;
A9:
the carrier of (Y1 union Y2) = C1 \/ C2
by TSEP_1:def 2;
hence
( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
by A10; verum