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 closed 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 open 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 closed 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 open 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 closed 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 open 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: now :: thesis: ( ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty closed 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 open 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 A3: ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty closed 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 open 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
A4: X1 is not SubSpace of X2 and
A5: X2 is not SubSpace of X1 ; :: thesis: X1,X2 are_weakly_separated
consider Y1, Y2 being non empty closed SubSpace of X such that
A6: Y1 meet (X1 union X2) is SubSpace of X1 and
A7: Y2 meet (X1 union X2) is SubSpace of X2 and
A8: ( X1 union X2 is SubSpace of Y1 union Y2 or ex Y being non empty open 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, A4, A5;
reconsider C2 = the carrier of Y2 as Subset of X by Th1;
reconsider C1 = the carrier of Y1 as Subset of X by Th1;
A9: the carrier of (X1 union X2) = A1 \/ A2 by Def2;
A10: 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 A11: C1 misses A1 \/ A2 by A9;

A12: 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 A9, A10, Th4;
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 A11, XBOOLE_0:def 7
.= C2 /\ (A1 \/ A2) ;
then C2 meets A1 \/ A2 by XBOOLE_0:def 7;
then Y2 meets X1 union X2 by A9;
then the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A9, Def4;
hence A1 \/ A2 c= A2 by A7, A13, 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 open SubSpace of X such that
A14: TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y and
A15: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A8;
reconsider C = the carrier of Y as Subset of X by Th1;
the carrier of X = (C1 \/ C2) \/ C by A10, A14, Def2;
then A16: 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 A11, XBOOLE_0:def 7
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23 ;

A17: 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 A9;
then A18: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A9, Def4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
then A19: C /\ (A1 \/ A2) c= A1 /\ A2 by A15, A18, Th4;
A20: A1 /\ A2 c= A2 by XBOOLE_1:17;
then A21: C /\ (A1 \/ A2) c= A2 by A19, 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 A16, A19, A20, 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 A9;
then the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A9, Def4;
then C2 /\ (A1 \/ A2) c= A2 by A7, Th4;
hence A1 \/ A2 c= A2 by A16, A21, 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 A9;
then A22: the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A9, Def4;
then A23: C2 /\ (A1 \/ A2) c= A2 by A7, 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 A7, A16, A22, 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 A9;
then A24: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A9, Def4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A15, A24, Th4;
then A1 \/ A2 c= A2 \/ (A1 /\ A2) by A16, A23, 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 A16, A17; :: thesis: verum

end;

end;

end;

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

end;

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

now :: thesis: Y2 meets X1 union X2

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

A27: 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 A9, A10, Th4;
then A28: A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ (C2 /\ (A1 \/ A2)) by XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ {} by A26, XBOOLE_0:def 7
.= C1 /\ (A1 \/ A2) ;
then C1 meets A1 \/ A2 by XBOOLE_0:def 7;
then Y1 meets X1 union X2 by A9;
then the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A9, Def4;
hence A1 \/ A2 c= A1 by A6, A28, 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 open SubSpace of X such that
A29: TopStruct(# the carrier of X, the topology of X #) = (Y1 union Y2) union Y and
A30: Y meet (X1 union X2) is SubSpace of X1 meet X2 by A8;
reconsider C = the carrier of Y as Subset of X by Th1;
the carrier of X = (C1 \/ C2) \/ C by A10, A29, Def2;
then A31: 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 A26, XBOOLE_0:def 7
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23 ;

A32: 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 A9;
then A33: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A9, Def4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
then A34: C /\ (A1 \/ A2) c= A1 /\ A2 by A30, A33, Th4;
A35: A1 /\ A2 c= A1 by XBOOLE_1:17;
then A36: C /\ (A1 \/ A2) c= A1 by A34, 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 A31, A34, A35, 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 A9;
then the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A9, Def4;
then C1 /\ (A1 \/ A2) c= A1 by A6, Th4;
hence A1 \/ A2 c= A1 by A31, A36, 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 A9;
then A37: the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A9, Def4;
then A38: C1 /\ (A1 \/ A2) c= A1 by A6, 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 A6, A31, A37, 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 A9;
then A39: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A9, Def4;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A30, A39, Th4;
then A1 \/ A2 c= A1 \/ (A1 /\ A2) by A31, A38, 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 A31, A32; :: thesis: verum

end;

end;

end;

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

end;

then the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A9, Def4;
then A40: C2 /\ (A1 \/ A2) c= A2 by A7, Th4;
A41: ( C1 is closed & C2 is closed ) by Th11;

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

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

suppose A42: 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 open )

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

proof

take C = (C1 \/ C2) ` ; :: thesis: ( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is open )
C misses A1 \/ A2 by A42, 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 open ) by A41, PRE_TOPC:2, XBOOLE_1:2; :: thesis: verum

end;

end;

suppose A43: 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 open )

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

proof

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

now :: thesis: Y meets X1 union X2

assume not Y meets X1 union X2 ; :: thesis: contradiction
then A47: C misses A1 \/ A2 by A9;
the carrier of X = (C1 \/ C2) \/ C by A10, A44, 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 A47, XBOOLE_0:def 7
.= (C1 \/ C2) /\ (A1 \/ A2) ;
hence contradiction by A43, XBOOLE_1:17; :: thesis: verum

end;

then A48: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A9, Def4;
A49: C is open by Th16;
the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
then C /\ (A1 \/ A2) c= A1 /\ A2 by A45, A48, Th4;
hence ex C being Subset of X st
( the carrier of X = (C1 \/ C2) \/ C & C /\ (A1 \/ A2) c= A1 /\ A2 & C is open ) by A49, A46; :: 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 A41, A25, A40, Th54;
hence X1,X2 are_weakly_separated ; :: thesis: verum

end;

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

end;

A50: 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 closed 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 open 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 closed 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 open 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 A51: 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 closed 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 open 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
A52: X1 is not SubSpace of X2 and
A53: X2 is not SubSpace of X1 ; :: thesis: ex Y1, Y2 being non empty closed 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 open 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 ) ) )
A54: not A2 c= A1 by A53, Th4;
A55: not A1 c= A2 by A52, Th4;
then consider C1, C2 being non empty Subset of X such that
A56: C1 is closed and
A57: C2 is closed and
A58: C1 /\ (A1 \/ A2) c= A1 and
A59: C2 /\ (A1 \/ A2) c= A2 and
A60: ( A1 \/ A2 c= C1 \/ C2 or ex C being non empty Subset of X st
( C is open & C /\ (A1 \/ A2) c= A1 /\ A2 & the carrier of X = (C1 \/ C2) \/ C ) ) by A51, A54, Th55;

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

assume C2 misses A1 \/ A2 ; :: thesis: contradiction
then A62: 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 A63: A1 \/ A2 c= C1 \/ C2 ; :: thesis: contradiction

A64: A2 c= A1 \/ A2 by XBOOLE_1:7;
A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A63, XBOOLE_1:28
.= (C1 /\ (A1 \/ A2)) \/ {} by A62, XBOOLE_1:23
.= C1 /\ (A1 \/ A2) ;
hence contradiction by A54, A58, A64, 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 open and
A65: C /\ (A1 \/ A2) c= A1 /\ A2 and
A66: the carrier of X = (C1 \/ C2) \/ C by A60;
A1 \/ A2 = ((C2 \/ C1) \/ C) /\ (A1 \/ A2) by A66, XBOOLE_1:28
.= (C2 \/ (C1 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C1 \/ C) /\ (A1 \/ A2)) by A62, XBOOLE_1:23
.= (C1 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23 ;
then A1 \/ A2 c= A1 \/ (A1 /\ A2) by A58, A65, XBOOLE_1:13;
then A67: A1 \/ A2 c= A1 by XBOOLE_1:12, XBOOLE_1:17;
A2 c= A1 \/ A2 by XBOOLE_1:7;
hence contradiction by A54, A67, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

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

assume C1 misses A1 \/ A2 ; :: thesis: contradiction
then A69: 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 A70: A1 \/ A2 c= C1 \/ C2 ; :: thesis: contradiction

A71: A1 c= A1 \/ A2 by XBOOLE_1:7;
A1 \/ A2 = (C1 \/ C2) /\ (A1 \/ A2) by A70, XBOOLE_1:28
.= {} \/ (C2 /\ (A1 \/ A2)) by A69, XBOOLE_1:23
.= C2 /\ (A1 \/ A2) ;
hence contradiction by A55, A59, A71, 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 open and
A72: C /\ (A1 \/ A2) c= A1 /\ A2 and
A73: the carrier of X = (C1 \/ C2) \/ C by A60;
A1 \/ A2 = ((C1 \/ C2) \/ C) /\ (A1 \/ A2) by A73, XBOOLE_1:28
.= (C1 \/ (C2 \/ C)) /\ (A1 \/ A2) by XBOOLE_1:4
.= {} \/ ((C2 \/ C) /\ (A1 \/ A2)) by A69, XBOOLE_1:23
.= (C2 /\ (A1 \/ A2)) \/ (C /\ (A1 \/ A2)) by XBOOLE_1:23 ;
then A1 \/ A2 c= A2 \/ (A1 /\ A2) by A59, A72, XBOOLE_1:13;
then A74: A1 \/ A2 c= A2 by XBOOLE_1:12, XBOOLE_1:17;
A1 c= A1 \/ A2 by XBOOLE_1:7;
hence contradiction by A55, A74, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

thus ex Y1, Y2 being non empty closed 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 open 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 closed SubSpace of X such that
A75: C2 = the carrier of Y2 by A57, Th15;
A76: the carrier of (X1 union X2) = A1 \/ A2 by Def2;
then Y2 meets X1 union X2 by A61, A75;
then A77: the carrier of (Y2 meet (X1 union X2)) = C2 /\ (A1 \/ A2) by A75, A76, Def4;
consider Y1 being non empty strict closed SubSpace of X such that
A78: C1 = the carrier of Y1 by A56, Th15;
A79: the carrier of (Y1 union Y2) = C1 \/ C2 by A78, A75, Def2;

A80: now :: thesis: ( X1 union X2 is not SubSpace of Y1 union Y2 implies ex Y being non empty open 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 A81: X1 union X2 is not SubSpace of Y1 union Y2 ; :: thesis: ex Y being non empty open 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
A82: C is open and
A83: C /\ (A1 \/ A2) c= A1 /\ A2 and
A84: the carrier of X = (C1 \/ C2) \/ C by A60, A76, A79, Th4;
A85: not A1 \/ A2 c= C1 \/ C2 by A76, A79, A81, Th4;
thus ex Y being non empty open 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 open SubSpace of X such that
A86: C = the carrier of Y by A82, Th20;

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

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

end;

then Y meets X1 union X2 by A76, A86;
then A88: the carrier of (Y meet (X1 union X2)) = C /\ (A1 \/ A2) by A76, A86, 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 )
A89: the carrier of (X1 meet X2) = A1 /\ A2 by A1, Def4;
the carrier of X = the carrier of (Y1 union Y2) \/ C by A78, A75, A84, Def2
.= the carrier of ((Y1 union Y2) union Y) by A86, 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 A50, A83, A88, A89, Th4, Th5; :: thesis: verum

end;

end;

take Y1 ; :: thesis: ex Y2 being non empty closed 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 open 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 open 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 A68, A78, A76;
then the carrier of (Y1 meet (X1 union X2)) = C1 /\ (A1 \/ A2) by A78, A76, 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 open 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 A58, A59, A77, A80, Th4; :: thesis: verum

end;

end;

hence ( X1 is SubSpace of X2 or X2 is SubSpace of X1 or ex Y1, Y2 being non empty closed 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 open 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 closed 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 open 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 A2; :: thesis: verum