let FT be non empty filled RelStr ; 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; ( 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
; ( 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 ) )
( ( 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 )
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 )
verumproof
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 )
;
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;
( 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
;
( 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;
verum
end;
hence
B is
connected
by A1, Th12;
verum
end;