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 )

Q = {} FT ) by Th3; :: thesis: verum

( 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 ) )

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 ( 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;( 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

Q = {} FT ) by Th3; :: thesis: verum