let FT be non empty filled RelStr ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 :: thesis: ( 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 ; :: thesis: 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; :: thesis: ex Q1 being Subset of FT st
( A = P1 \/ Q1 & P1 misses Q1 & P1,Q1 are_separated & P1 <> {} FT & Q1 <> {} FT )
take Q1 = Q1; :: thesis: ( 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; :: thesis: ( 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; :: thesis: 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; :: thesis: verum