let FT be non empty RelStr ; :: thesis: for A being non empty Subset of FT holds

( A is connected iff FT | A is connected )

let A be non empty Subset of FT; :: thesis: ( A is connected iff FT | A is connected )

A1: [#] (FT | A) = A by Def3;

thus ( A is connected implies FT | A is connected ) :: thesis: ( FT | A is connected implies A is connected )

then A5: [#] (FT | A) is connected ;

let B, C be Subset of FT; :: according to FIN_TOPO:def 16 :: thesis: ( not A = B \/ C or B = {} or C = {} or not B misses C or not B ^b misses C )

assume that

A6: A = B \/ C and

A7: ( B <> {} & C <> {} & B misses C ) ; :: thesis: not B ^b misses C

A8: [#] (FT | A) = A by Def3;

then reconsider B2 = B as Subset of (FT | A) by A6, XBOOLE_1:7;

reconsider C2 = C as Subset of (FT | A) by A6, A8, XBOOLE_1:7;

( ([#] (FT | A)) /\ C2 = C2 & B2 ^b = (B ^b) /\ ([#] (FT | A)) ) by Th12, XBOOLE_1:28;

then A9: (B ^b) /\ C = (B2 ^b) /\ C2 by XBOOLE_1:16;

B2 ^b meets C2 by A5, A6, A7, A8;

hence (B ^b) /\ C <> {} by A9; :: according to XBOOLE_0:def 7 :: thesis: verum

( A is connected iff FT | A is connected )

let A be non empty Subset of FT; :: thesis: ( A is connected iff FT | A is connected )

A1: [#] (FT | A) = A by Def3;

thus ( A is connected implies FT | A is connected ) :: thesis: ( FT | A is connected implies A is connected )

proof

assume
FT | A is connected
; :: thesis: A is connected
assume A2:
A is connected
; :: thesis: FT | A is connected

for B2, C2 being Subset of (FT | A) st [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 holds

B2 ^b meets C2

hence FT | A is connected ; :: thesis: verum

end;for B2, C2 being Subset of (FT | A) st [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 holds

B2 ^b meets C2

proof

then
[#] (FT | A) is connected
;
let B2, C2 be Subset of (FT | A); :: thesis: ( [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 implies B2 ^b meets C2 )

A3: ([#] (FT | A)) /\ C2 = C2 by XBOOLE_1:28;

the carrier of (FT | A) = [#] (FT | A)

.= A by Def3 ;

then reconsider B3 = B2, C3 = C2 as Subset of FT by XBOOLE_1:1;

assume ( [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 ) ; :: thesis: B2 ^b meets C2

then A4: B3 ^b meets C3 by A1, A2;

(B2 ^b) /\ C2 = ((B3 ^b) /\ ([#] (FT | A))) /\ C2 by Th12

.= (B3 ^b) /\ C3 by A3, XBOOLE_1:16 ;

then (B2 ^b) /\ C2 <> {} by A4;

hence B2 ^b meets C2 ; :: thesis: verum

end;A3: ([#] (FT | A)) /\ C2 = C2 by XBOOLE_1:28;

the carrier of (FT | A) = [#] (FT | A)

.= A by Def3 ;

then reconsider B3 = B2, C3 = C2 as Subset of FT by XBOOLE_1:1;

assume ( [#] (FT | A) = B2 \/ C2 & B2 <> {} & C2 <> {} & B2 misses C2 ) ; :: thesis: B2 ^b meets C2

then A4: B3 ^b meets C3 by A1, A2;

(B2 ^b) /\ C2 = ((B3 ^b) /\ ([#] (FT | A))) /\ C2 by Th12

.= (B3 ^b) /\ C3 by A3, XBOOLE_1:16 ;

then (B2 ^b) /\ C2 <> {} by A4;

hence B2 ^b meets C2 ; :: thesis: verum

hence FT | A is connected ; :: thesis: verum

then A5: [#] (FT | A) is connected ;

let B, C be Subset of FT; :: according to FIN_TOPO:def 16 :: thesis: ( not A = B \/ C or B = {} or C = {} or not B misses C or not B ^b misses C )

assume that

A6: A = B \/ C and

A7: ( B <> {} & C <> {} & B misses C ) ; :: thesis: not B ^b misses C

A8: [#] (FT | A) = A by Def3;

then reconsider B2 = B as Subset of (FT | A) by A6, XBOOLE_1:7;

reconsider C2 = C as Subset of (FT | A) by A6, A8, XBOOLE_1:7;

( ([#] (FT | A)) /\ C2 = C2 & B2 ^b = (B ^b) /\ ([#] (FT | A)) ) by Th12, XBOOLE_1:28;

then A9: (B ^b) /\ C = (B2 ^b) /\ C2 by XBOOLE_1:16;

B2 ^b meets C2 by A5, A6, A7, A8;

hence (B ^b) /\ C <> {} by A9; :: according to XBOOLE_0:def 7 :: thesis: verum