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 that
A3: C c= B and
A4: C ^b misses B \ C ; :: thesis: ( C = {} or B \ C = {} )
C misses (B \ C) ^b by A1, A4, Th8;
then A5: C,B \ C are_separated by A4;
C \/ (B \ C) = C \/ B by XBOOLE_1:39
.= B by A3, XBOOLE_1:12 ;
then ( C = B or B \ C = B ) by A1, A2, A5, 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 A6: 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 that
A7: B = A \/ B2 and
A8: A,B2 are_separated ; :: thesis: ( A = B or B2 = B )
A9: (A \/ B2) \ A = B2 \ A by XBOOLE_1:40;
A ^b misses B2 by A8;
then A ^b misses B \ A by A7, A9, XBOOLE_1:36, XBOOLE_1:63;
then ( A = {} or B \ A = {} ) by A6, A7, XBOOLE_1:7;
then A10: ( B = B2 or B c= A ) by A7, XBOOLE_1:37;
A c= B by A7, XBOOLE_1:7;
hence ( A = B or B2 = B ) by A10, XBOOLE_0:def 10; :: thesis: verum
end;
hence B is connected by A1, Th12; :: thesis: verum
end;