let FT be non empty filled RelStr ; :: thesis: for IT being Subset of FT st FT is symmetric holds
( 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 )
let IT be Subset of FT; :: thesis: ( FT is symmetric implies ( 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 ) )
assume A1: FT is symmetric ; :: thesis: ( 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 )

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

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

proof

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

now :: thesis: not A ^b misses B

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

now :: thesis: not A meets B ^b

assume A meets B ^b ; :: thesis: contradiction
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: verum

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: verum

end;

hence A ^b meets B ; :: thesis: verum

end;

hence IT is connected ; :: thesis: verum

end;

now :: thesis: ( IT is connected implies for A, B being Subset of FT st IT = A \/ B & A,B are_separated & not A = IT holds
B = IT )

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

proof

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

now :: thesis: ( A <> {} & not A = IT implies B = IT )

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

end;

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

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: verum