let X be non empty TopSpace; for X1, X2, Y1, Y2 being non empty SubSpace of X st X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is SubSpace of Y1 union Y2 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 holds
( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
let X1, X2, Y1, Y2 be non empty SubSpace of X; ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 & X1 union X2 is SubSpace of Y1 union Y2 & Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 implies ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume that
A1:
X1 is not SubSpace of X2
and
A2:
X2 is not SubSpace of X1
; ( not X1 union X2 is SubSpace of Y1 union Y2 or not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
reconsider A1 = the carrier of X1, A2 = the carrier of X2, C1 = the carrier of Y1, C2 = the carrier of Y2 as Subset of X by TSEP_1:1;
assume A3:
X1 union X2 is SubSpace of Y1 union Y2
; ( not Y1 meet (X1 union X2) is SubSpace of X1 or not Y2 meet (X1 union X2) is SubSpace of X2 or ( Y1 meets X1 union X2 & Y2 meets X1 union X2 ) )
assume that
A4:
Y1 meet (X1 union X2) is SubSpace of X1
and
A5:
Y2 meet (X1 union X2) is SubSpace of X2
; ( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
A6:
the carrier of (X1 union X2) = A1 \/ A2
by TSEP_1:def 2;
A7:
the carrier of (Y1 union Y2) = C1 \/ C2
by TSEP_1:def 2;
A8:
now not Y2 misses X1 union X2assume
Y2 misses X1 union X2
;
contradictionthen A9:
C2 misses A1 \/ A2
by A6, TSEP_1:def 3;
A1 \/ A2 c= C1 \/ C2
by A3, A6, A7, TSEP_1:4;
then A10:
A1 \/ A2 =
(C1 \/ C2) /\ (A1 \/ A2)
by XBOOLE_1:28
.=
(C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2))
by XBOOLE_1:23
.=
C1 /\ (A1 \/ A2)
by A9
;
then
C1 meets A1 \/ A2
;
then
Y1 meets X1 union X2
by A6, TSEP_1:def 3;
then
the
carrier of
(Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2)
by A6, TSEP_1:def 4;
then A11:
A1 \/ A2 c= A1
by A4, A10, TSEP_1:4;
A2 c= A1 \/ A2
by XBOOLE_1:7;
hence
contradiction
by A2, TSEP_1:4, A11, XBOOLE_1:1;
verum end;
now not Y1 misses X1 union X2assume
Y1 misses X1 union X2
;
contradictionthen A12:
C1 misses A1 \/ A2
by A6, TSEP_1:def 3;
A1 \/ A2 c= C1 \/ C2
by A3, A6, A7, TSEP_1:4;
then A13:
A1 \/ A2 =
(C1 \/ C2) /\ (A1 \/ A2)
by XBOOLE_1:28
.=
(C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2))
by XBOOLE_1:23
.=
C2 /\ (A1 \/ A2)
by A12
;
then
C2 meets A1 \/ A2
;
then
Y2 meets X1 union X2
by A6, TSEP_1:def 3;
then
the
carrier of
(Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2)
by A6, TSEP_1:def 4;
then A14:
A1 \/ A2 c= A2
by A5, A13, TSEP_1:4;
A1 c= A1 \/ A2
by XBOOLE_1:7;
then
A1 c= A2
by A14, XBOOLE_1:1;
hence
contradiction
by A1, TSEP_1:4;
verum end;
hence
( Y1 meets X1 union X2 & Y2 meets X1 union X2 )
by A8; verum