let X be non empty TopSpace; :: thesis: for X1, X2 being non empty SubSpace of X st X1 meets X2 holds
( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) )
let X1, X2 be non empty SubSpace of X; :: thesis: ( X1 meets X2 implies ( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) ) )
reconsider A2 = the carrier of X2 as Subset of X by Th1;
reconsider A1 = the carrier of X1 as Subset of X by Th1;
assume A1: X1 meets X2 ; :: thesis: ( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) )
A2: [#] X = the carrier of X ;

A3: now :: thesis: ( ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) implies X1,X2 are_weakly_separated )

assume A4: ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) ; :: thesis: X1,X2 are_weakly_separated

now :: thesis: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 implies X1,X2 are_weakly_separated )

assume that
A5: X1 is not SubSpace of X2 and
A6: X2 is not SubSpace of X1 ; :: thesis: X1,X2 are_weakly_separated
consider Y1, Y2 being non empty open SubSpace of X such that
A7: Y1 meet (X1 union X2) is SubSpace of X1 and
A8: Y2 meet (X1 union X2) is SubSpace of X2 and
A9: ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) by A4, A5, A6;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
A10: the carrier of (X1 union X2) = A1 \/ A2 by Def2;
A11: the carrier of (Y1 union Y2) = C1 \/ C2 by Def2;

now :: thesis: not Y1 misses X1 union X2

assume Y1 misses X1 union X2 ; :: thesis: contradiction
then A12: C1 misses A1 \/ A2 by A10;

A13: now :: thesis: A1 \/ A2 c= A2

per cases ( X1 union X2 is SubSpace of Y1 union Y2 or not X1 union X2 is SubSpace of Y1 union Y2 ) ;

suppose X1 union X2 is SubSpace of Y1 union Y2 ; :: thesis: A1 \/ A2 c= A2

then A1 \/ A2 c= C1 \/ C2 by A10, A11, Th4;
then A14: 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, XBOOLE_0:def 7
.= C2 /\ (A1 \/ A2) ;
then C2 meets A1 \/ A2 by XBOOLE_0:def 7;
then Y2 meets X1 union X2 by A10;
then the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A10, Def4;
hence A1 \/ A2 c= A2 by A8, A14, Th4; :: thesis: verum

end;

suppose X1 union X2 is not SubSpace of Y1 union Y2 ; :: thesis: A1 \/ A2 c= A2

then consider Y being non empty closed SubSpace of X such that
A15: TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y and
A16: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A9;
reconsider C = the carrier of Y as Subset of X by Th1;
the carrier of X = (C1 \/ C2) \/ C by A11, A15, Def2;
then A17: A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C1 /\ (A1 \/ A2)) \/ ((C2 \/ C) /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A12, XBOOLE_0:def 7
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23 ;

A18: now :: thesis: ( C /\ (A1 \/ A2) <> {} implies A1 \/ A2 c= A2 )

assume C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2
then C meets A1 \/ A2 by XBOOLE_0:def 7;
then Y meets X1 union X2 by A10;
then A19: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A10, Def4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
then A20: C /\ (A1 \/ A2) c= A1 /\ A2 by A16, A19, Th4;
A21: A1 /\ A2 c= A2 by XBOOLE_1:17;
then A22: C /\ (A1 \/ A2) c= A2 by A20, XBOOLE_1:1;

now :: thesis: A1 \/ A2 c= A2

per cases ( C2 /\ (A1 \/ A2) = {} or C2 /\ (A1 \/ A2) <> {} ) ;

suppose C2 /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A2

hence A1 \/ A2 c= A2 by A17, A20, A21, XBOOLE_1:1; :: thesis: verum

end;

suppose C2 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2

then C2 meets A1 \/ A2 by XBOOLE_0:def 7;
then Y2 meets X1 union X2 by A10;
then the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A10, Def4;
then C2 /\ (A1 \/ A2) c= A2 by A8, Th4;
hence A1 \/ A2 c= A2 by A17, A22, XBOOLE_1:8; :: thesis: verum

end;

end;

end;

hence A1 \/ A2 c= A2 ; :: thesis: verum

end;

now :: thesis: ( C2 /\ (A1 \/ A2) <> {} implies A1 \/ A2 c= A2 )

assume C2 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2
then C2 meets A1 \/ A2 by XBOOLE_0:def 7;
then Y2 meets X1 union X2 by A10;
then A23: the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A10, Def4;
then A24: C2 /\ (A1 \/ A2) c= A2 by A8, Th4;

now :: thesis: A1 \/ A2 c= A2

per cases ( C /\ (A1 \/ A2) = {} or C /\ (A1 \/ A2) <> {} ) ;

suppose C /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A2

hence A1 \/ A2 c= A2 by A8, A17, A23, Th4; :: thesis: verum

end;

suppose C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A2

then C meets A1 \/ A2 by XBOOLE_0:def 7;
then Y meets X1 union X2 by A10;
then A25: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A10, Def4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A16, A25, Th4;
then A1 \/ A2 c= A2 \/ (A1 /\ A2) by A17, A24, XBOOLE_1:13;
hence A1 \/ A2 c= A2 by XBOOLE_1:12, XBOOLE_1:17; :: thesis: verum

end;

end;

end;

hence A1 \/ A2 c= A2 ; :: thesis: verum

end;

hence A1 \/ A2 c= A2 by A17, A18; :: thesis: verum

end;

end;

end;

A1 c= A1 \/ A2 by XBOOLE_1:7;
then A1 c= A2 by A13, XBOOLE_1:1;
hence contradiction by A5, Th4; :: thesis: verum

end;

then the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A10, Def4;
then A26: C1 /\ (A1 \/ A2) c= A1 by A7, Th4;

now :: thesis: Y2 meets X1 union X2

assume not Y2 meets X1 union X2 ; :: thesis: contradiction
then A27: C2 misses A1 \/ A2 by A10;

A28: now :: thesis: A1 \/ A2 c= A1

per cases ( X1 union X2 is SubSpace of Y1 union Y2 or not X1 union X2 is SubSpace of Y1 union Y2 ) ;

suppose X1 union X2 is SubSpace of Y1 union Y2 ; :: thesis: A1 \/ A2 c= A1

then A1 \/ A2 c= C1 \/ C2 by A10, A11, Th4;
then A29: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ {} by A27, XBOOLE_0:def 7
.= C1 /\ (A1 \/ A2) ;
then C1 meets A1 \/ A2 by XBOOLE_0:def 7;
then Y1 meets X1 union X2 by A10;
then the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A10, Def4;
hence A1 \/ A2 c= A1 by A7, A29, Th4; :: thesis: verum

end;

suppose X1 union X2 is not SubSpace of Y1 union Y2 ; :: thesis: A1 \/ A2 c= A1

then consider Y being non empty closed SubSpace of X such that
A30: TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y and
A31: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A9;
reconsider C = the carrier of Y as Subset of X by Th1;
the carrier of X = (C1 \/ C2) \/ C by A11, A30, Def2;
then A32: A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= (C2 /\ (A1 \/ A2)) \/ ((C1 \/ C) /\ (A1 \/ A2)) by XBOOLE_1:23
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A27, XBOOLE_0:def 7
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23 ;

A33: now :: thesis: ( C /\ (A1 \/ A2) <> {} implies A1 \/ A2 c= A1 )

assume C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1
then C meets A1 \/ A2 by XBOOLE_0:def 7;
then Y meets X1 union X2 by A10;
then A34: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A10, Def4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
then A35: C /\ (A1 \/ A2) c= A1 /\ A2 by A31, A34, Th4;
A36: A1 /\ A2 c= A1 by XBOOLE_1:17;
then A37: C /\ (A1 \/ A2) c= A1 by A35, XBOOLE_1:1;

now :: thesis: A1 \/ A2 c= A1

per cases ( C1 /\ (A1 \/ A2) = {} or C1 /\ (A1 \/ A2) <> {} ) ;

suppose C1 /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A1

hence A1 \/ A2 c= A1 by A32, A35, A36, XBOOLE_1:1; :: thesis: verum

end;

suppose C1 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1

then C1 meets A1 \/ A2 by XBOOLE_0:def 7;
then Y1 meets X1 union X2 by A10;
then the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A10, Def4;
then C1 /\ (A1 \/ A2) c= A1 by A7, Th4;
hence A1 \/ A2 c= A1 by A32, A37, XBOOLE_1:8; :: thesis: verum

end;

end;

end;

hence A1 \/ A2 c= A1 ; :: thesis: verum

end;

now :: thesis: ( C1 /\ (A1 \/ A2) <> {} implies A1 \/ A2 c= A1 )

assume C1 /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1
then C1 meets A1 \/ A2 by XBOOLE_0:def 7;
then Y1 meets X1 union X2 by A10;
then A38: the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A10, Def4;
then A39: C1 /\ (A1 \/ A2) c= A1 by A7, Th4;

now :: thesis: A1 \/ A2 c= A1

per cases ( C /\ (A1 \/ A2) = {} or C /\ (A1 \/ A2) <> {} ) ;

suppose C /\ (A1 \/ A2) = {} ; :: thesis: A1 \/ A2 c= A1

hence A1 \/ A2 c= A1 by A7, A32, A38, Th4; :: thesis: verum

end;

suppose C /\ (A1 \/ A2) <> {} ; :: thesis: A1 \/ A2 c= A1

then C meets A1 \/ A2 by XBOOLE_0:def 7;
then Y meets X1 union X2 by A10;
then A40: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A10, Def4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A31, A40, Th4;
then A1 \/ A2 c= A1 \/ (A1 /\ A2) by A32, A39, XBOOLE_1:13;
hence A1 \/ A2 c= A1 by XBOOLE_1:12, XBOOLE_1:17; :: thesis: verum

end;

end;

end;

hence A1 \/ A2 c= A1 ; :: thesis: verum

end;

hence A1 \/ A2 c= A1 by A32, A33; :: thesis: verum

end;

end;

end;

A2 c= A1 \/ A2 by XBOOLE_1:7;
then A2 c= A1 by A28, XBOOLE_1:1;
hence contradiction by A6, Th4; :: thesis: verum

end;

then the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A10, Def4;
then A41: C2 /\ (A1 \/ A2) c= A2 by A8, Th4;
A42: ( C1 is open & C2 is open ) by Th16;

now :: thesis: ex C being Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed )

per cases ( A1 \/ A2 c= C1 \/ C2 or not A1 \/ A2 c= C1 \/ C2 ) ;

suppose A43: A1 \/ A2 c= C1 \/ C2 ; :: thesis: ex C being Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed )

thus ex C being Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed ) :: thesis: verum

proof

take C = (C1 \/ C2) ` ; :: thesis: ( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed )
C misses A1 \/ A2 by A43, SUBSET_1:24;
then C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
hence ( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed ) by A2, A42, PRE_TOPC:2, XBOOLE_1:2; :: thesis: verum

end;

end;

suppose A44: not A1 \/ A2 c= C1 \/ C2 ; :: thesis: ex C being Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed )

thus ex C being Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed ) :: thesis: verum

proof

consider Y being non empty closed SubSpace of X such that
A45: TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y and
A46: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A9, A10, A11, A44, Th4;
reconsider C = the carrier of Y as Subset of X by Th1;
A47: the carrier of X = the carrier of (Y1 union Y2) \/ C by A45, Def2
.= (C1 \/ C2) \/ C by Def2 ;

now :: thesis: Y meets X1 union X2

assume not Y meets X1 union X2 ; :: thesis: contradiction
then A48: C misses A1 \/ A2 by A10;
the carrier of X = (C1 \/ C2) \/ C by A11, A45, Def2;
then A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by XBOOLE_1:28
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A48, XBOOLE_0:def 7
.= (C1 \/ C2) /\ (A1 \/ A2) ;
hence contradiction by A44, XBOOLE_1:17; :: thesis: verum

end;

then A49: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A10, Def4;
A50: C is closed by Th11;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A46, A49, Th4;
hence ex C being Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is closed ) by A50, A47; :: thesis: verum

end;

end;

end;

end;

then for A1, A2 being Subset of X st A1 = the carrier of X1 & A2 = the carrier of X2 holds
A1,A2 are_weakly_separated by A42, A26, A41, Th58;
hence X1,X2 are_weakly_separated ; :: thesis: verum

end;

hence X1,X2 are_weakly_separated by Th79; :: thesis: verum

end;

A51: X is SubSpace of X by Th2;

now :: thesis: ( not X1,X2 are_weakly_separated or X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) )

assume X1,X2 are_weakly_separated ; :: thesis: ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) )
then A52: A1,A2 are_weakly_separated ;

now :: thesis: ( X1 is not SubSpace of X2 & X2 is not SubSpace of X1 implies ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) )

assume that
A53: X1 is not SubSpace of X2 and
A54: X2 is not SubSpace of X1 ; :: thesis: ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) )
A55: not A2 c= A1 by A54, Th4;
A56: not A1 c= A2 by A53, Th4;
then consider C1, C2 being non empty Subset of X such that
A57: C1 is open and
A58: C2 is open and
A59: C1 /\ (A1 \/ A2) c= A1 and
A60: C2 /\ (A1 \/ A2) c= A2 and
A61: ( A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
( C is closed & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C ) ) by A52, A55, Th59;

A62: now :: thesis: not C2 misses A1 \/ A2

assume C2 misses A1 \/ A2 ; :: thesis: contradiction
then A63: C2 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;

now :: thesis: contradiction

per cases ( A1 \/ A2 c= C1 \/ C2 or not A1 \/ A2 c= C1 \/ C2 ) ;

suppose A64: A1 \/ A2 c= C1 \/ C2 ; :: thesis: contradiction

A65: A2 c= A1 \/ A2 by XBOOLE_1:7;
A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A64, XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ {} by A63, XBOOLE_1:23
.= C1 /\ (A1 \/ A2) ;
hence contradiction by A55, A59, A65, XBOOLE_1:1; :: thesis: verum

end;

suppose not A1 \/ A2 c= C1 \/ C2 ; :: thesis: contradiction

then consider C being non empty Subset of X such that
C is closed and
A66: C /\ (A1 \/ A2) c= A1 /\ A2 and
A67: the carrier of X = (C1 \/ C2) \/ C by A61;
A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A67, XBOOLE_1:28
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A63, XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23 ;
then A1 \/ A2 c= A1 \/ (A1 /\ A2) by A59, A66, XBOOLE_1:13;
then A68: A1 \/ A2 c= A1 by XBOOLE_1:12, XBOOLE_1:17;
A2 c= A1 \/ A2 by XBOOLE_1:7;
hence contradiction by A55, A68, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

A69: now :: thesis: not C1 misses A1 \/ A2

assume C1 misses A1 \/ A2 ; :: thesis: contradiction
then A70: C1 /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;

now :: thesis: contradiction

per cases ( A1 \/ A2 c= C1 \/ C2 or not A1 \/ A2 c= C1 \/ C2 ) ;

suppose A71: A1 \/ A2 c= C1 \/ C2 ; :: thesis: contradiction

A72: A1 c= A1 \/ A2 by XBOOLE_1:7;
A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A71, XBOOLE_1:28
.= {} \/ (C2 /\ (A1 \/ A2)) by A70, XBOOLE_1:23
.= C2 /\ (A1 \/ A2) ;
hence contradiction by A56, A60, A72, XBOOLE_1:1; :: thesis: verum

end;

suppose not A1 \/ A2 c= C1 \/ C2 ; :: thesis: contradiction

then consider C being non empty Subset of X such that
C is closed and
A73: C /\ (A1 \/ A2) c= A1 /\ A2 and
A74: the carrier of X = (C1 \/ C2) \/ C by A61;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A74, XBOOLE_1:28
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A70, XBOOLE_1:23
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23 ;
then A1 \/ A2 c= A2 \/ (A1 /\ A2) by A60, A73, XBOOLE_1:13;
then A75: A1 \/ A2 c= A2 by XBOOLE_1:12, XBOOLE_1:17;
A1 c= A1 \/ A2 by XBOOLE_1:7;
hence contradiction by A56, A75, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

thus ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) :: thesis: verum

proof

consider Y2 being non empty strict open SubSpace of X such that
A76: C2 = the carrier of Y2 by A58, Th20;
A77: the carrier of (X1 union X2) = A1 \/ A2 by Def2;
then Y2 meets X1 union X2 by A62, A76;
then A78: the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A76, A77, Def4;
consider Y1 being non empty strict open SubSpace of X such that
A79: C1 = the carrier of Y1 by A57, Th20;
A80: the carrier of (Y1 union Y2) = C1 \/ C2 by A79, A76, Def2;

A81: now :: thesis: ( X1 union X2 is not SubSpace of Y1 union Y2 implies ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) )

assume A82: X1 union X2 is not SubSpace of Y1 union Y2 ; :: thesis: ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 )
then consider C being non empty Subset of X such that
A83: C is closed and
A84: C /\ (A1 \/ A2) c= A1 /\ A2 and
A85: the carrier of X = (C1 \/ C2) \/ C by A61, A77, A80, Th4;
A86: not A1 \/ A2 c= C1 \/ C2 by A77, A80, A82, Th4;
thus ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) :: thesis: verum

proof

consider Y being non empty strict closed SubSpace of X such that
A87: C = the carrier of Y by A83, Th15;

now :: thesis: not C misses A1 \/ A2

assume C misses A1 \/ A2 ; :: thesis: contradiction
then A88: C /\ (A1 \/ A2) = {} by XBOOLE_0:def 7;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A85, XBOOLE_1:28
.= ((C1 \/ C2) /\ (A1 \/ A2)) \/ {} by A88, XBOOLE_1:23
.= (C1 \/ C2) /\ (A1 \/ A2) ;
hence contradiction by A86, XBOOLE_1:17; :: thesis: verum

end;

then Y meets X1 union X2 by A77, A87;
then A89: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A77, A87, Def4;
take Y ; :: thesis: ( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 )
A90: the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
the carrier of X = the carrier of (Y1 union Y2) \/ C by A79, A76, A85, Def2
.= the carrier of ((Y1 union Y2) union Y) by A87, Def2 ;
hence ( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) by A51, A84, A89, A90, Th4, Th5; :: thesis: verum

end;

end;

take Y1 ; :: thesis: ex Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) )
take Y2 ; :: thesis: ( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) )
Y1 meets X1 union X2 by A69, A79, A77;
then the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A79, A77, Def4;
hence ( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) by A59, A60, A78, A81, Th4; :: thesis: verum

end;

end;

hence ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) ; :: thesis: verum

end;

hence ( X1,X2 are_weakly_separated iff ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty open SubSpace of X st
( Y1 meet (X1 union X2) is SubSpace of X1 & Y2 meet (X1 union X2) is SubSpace of X2 & ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty closed SubSpace of X st
( TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y & Y meet (X1 union X2) is SubSpace of X1 meet X2 ) ) ) ) ) by A3; :: thesis: verum