let FT be non empty filled RelStr ; for A being non empty Subset of FT st FT is symmetric holds
( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT )
let A be non empty Subset of FT; ( FT is symmetric implies ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT ) )
assume A1:
FT is symmetric
; ( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT )
now ( not A is connected implies ex P1, Q1 being Subset of FT st
( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT ) )assume
not
A is
connected
;
ex P1, Q1 being Subset of FT st
( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT )then
not
FT | A is
connected
by Th15;
then
not
[#] (FT | A) is
connected
;
then consider P,
Q being
Subset of
(FT | A) such that A2:
[#] (FT | A) = P \/ Q
and A3:
(
P <> {} &
Q <> {} )
and A4:
P misses Q
and A5:
P ^b misses Q
;
reconsider P1 =
P,
Q1 =
Q as
Subset of
FT by Th9;
take P1 =
P1;
ex Q1 being Subset of FT st
( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT )take Q1 =
Q1;
( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT )thus
(
A = P1 \/ Q1 &
P1 misses Q1 )
by A2, A4, Def3;
( P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT )A6:
P ^b = (P1 ^b) /\ ([#] (FT | A))
by Th12;
([#] (FT | A)) /\ Q1 = Q1
by XBOOLE_1:28;
then (P1 ^b) /\ Q1 =
((P1 ^b) /\ ([#] (FT | A))) /\ Q
by XBOOLE_1:16
.=
{}
by A5, A6
;
then
P1 ^b misses Q1
;
hence
(
P1,
Q1 are_separated &
P1 <> {} FT &
Q1 <> {} FT )
by A1, A3, FINTOPO4:10;
verum end;
hence
( A is connected iff for P, Q being Subset of FT st A = P \/ Q & P misses Q & P,Q are_separated & not P = {} FT holds
Q = {} FT )
by Th3; verum