let FT be non empty filled RelStr ; :: thesis: for B being Subset of FT st FT is symmetric holds
( B is connected iff for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) )
let B be Subset of FT; :: thesis: ( FT is symmetric implies ( B is connected iff for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ) )
assume A1: FT is symmetric ; :: thesis: ( B is connected iff for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) )
thus ( B is connected implies for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ) :: thesis: ( ( for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ) implies B is connected )

proof

assume A2: B is connected ; :: thesis: for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C )
for C being Subset of FT st C c= B & C ^b misses B \ C & not C = {} holds
B \ C = {}

proof

let C be Subset of FT; :: thesis: ( C c= B & C ^b misses B \ C & not C = {} implies B \ C = {} )
assume A3: ( C c= B & C ^b misses B \ C ) ; :: thesis: ( C = {} or B \ C = {} )
A4: C \/ (B \ C) = C \/ B by XBOOLE_1:39
.= B by A3, XBOOLE_1:12 ;
( C ^b misses B \ C & C misses (B \ C) ^b ) by A1, A3, Th8;
then C,B \ C are_separated by Def1;
then ( C = B or B \ C = B ) by A1, A2, A4, Th12;
hence ( C = {} or B \ C = {} ) by A3, XBOOLE_1:37, XBOOLE_1:38; :: thesis: verum

end;

hence for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ; :: thesis: verum

end;

thus ( ( for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ) implies B is connected ) :: thesis: verum

proof

assume A5: for C being Subset of FT holds
( not C <> {} or not B \ C <> {} or not C c= B or not C ^b misses B \ C ) ; :: thesis: B is connected
for A, B2 being Subset of FT st B = A \/ B2 & A,B2 are_separated & not A = B holds
B2 = B

proof

let A, B2 be Subset of FT; :: thesis: ( B = A \/ B2 & A,B2 are_separated & not A = B implies B2 = B )
assume A6: ( B = A \/ B2 & A,B2 are_separated ) ; :: thesis: ( A = B or B2 = B )
then A7: A c= B by XBOOLE_1:7;
A8: ( A ^b misses B2 & A misses B2 ^b ) by A6, Def1;
(A \/ B2) \ A = B2 \ A by XBOOLE_1:40;
then A ^b misses B \ A by A6, A8, XBOOLE_1:36, XBOOLE_1:63;
then ( A = {} or B \ A = {} ) by A5, A6, XBOOLE_1:7;
then ( B = B2 or B c= A ) by A6, XBOOLE_1:37;
hence ( A = B or B2 = B ) by A7, XBOOLE_0:def 10; :: thesis: verum

end;

hence B is connected by A1, Th12; :: thesis: verum

end;