let FT be non empty filled RelStr ; :: thesis:
let IT be Subset of FT; :: thesis:
assume A1: FT is symmetric ; :: thesis:

A2: now :: thesis:

assume A3: for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT ; :: thesis:
for A, B being Subset of FT st IT = A \/ B & A <> {} & B <> {} & A misses B holds
A ^b meets B

let A, B be Subset of FT; :: thesis:
assume that
A4: IT = A \/ B and
A5: ( A <> {} & B <> {} ) and
A misses B ; :: thesis:

assume A6: A ^b misses B ; :: thesis:

assume A meets B ^b ; :: thesis:
then consider x being object such that
A7: x in A and
A8: x in B ^b by XBOOLE_0:3;
consider x2 being Element of FT such that
A9: x2 = x and
A10: U_FT x2 meets B by A8;
set y = the Element of (U_FT x2) /\ B;
A11: (U_FT x2) /\ B <> {} by A10, XBOOLE_0:def 7;
then A12: the Element of (U_FT x2) /\ B in U_FT x2 by XBOOLE_0:def 4;
then reconsider y2 = the Element of (U_FT x2) /\ B as Element of FT ;
x2 in U_FT y2 by A1, A12;
then x2 in (U_FT y2) /\ A by A7, A9, XBOOLE_0:def 4;
then U_FT y2 meets A by XBOOLE_0:def 7;
then A13: y2 in A ^b ;
the Element of (U_FT x2) /\ B in B by A11, XBOOLE_0:def 4;
hence contradiction by A6, A13, XBOOLE_0:3; :: thesis:

end;

then A,B are_separated by A6;
then A14: ( A = IT or B = IT ) by A3, A4;
A15: A c= A ^b by FIN_TOPO:13;
(A ^b) /\ B = {} by A6, XBOOLE_0:def 7;
then A /\ B = {} by A15, XBOOLE_1:3, XBOOLE_1:26;
hence contradiction by A4, A5, A14, XBOOLE_1:21; :: thesis:

end;

hence A ^b meets B ; :: thesis:

end;

hence IT is connected ; :: thesis:

end;

assume A16: IT is connected ; :: thesis:
thus for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT :: thesis:

let A, B be Subset of FT; :: thesis:
assume that
A17: IT = A \/ B and
A18: A,B are_separated ; :: thesis:
A19: A misses B by A18, Th6;

assume A <> {} ; :: thesis:
then B = {} by A18, A16, A17, A19;
hence ( A = IT or B = IT ) by A17; :: thesis:

end;

hence ( A = IT or B = IT ) by A17; :: thesis:

end;

end;

hence ( IT is connected iff for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT ) by A2; :: thesis: