let FT be non empty RelStr ; :: thesis: for X9 being non empty SubSpace of FT

for A being Subset of FT

for B being Subset of X9 st A = B holds

( A is connected iff B is connected )

let X9 be non empty SubSpace of FT; :: thesis: for A being Subset of FT

for B being Subset of X9 st A = B holds

( A is connected iff B is connected )

let A8 be Subset of FT; :: thesis: for B being Subset of X9 st A8 = B holds

( A8 is connected iff B is connected )

let B8 be Subset of X9; :: thesis: ( A8 = B8 implies ( A8 is connected iff B8 is connected ) )

assume A1: A8 = B8 ; :: thesis: ( A8 is connected iff B8 is connected )

for A being Subset of FT

for B being Subset of X9 st A = B holds

( A is connected iff B is connected )

let X9 be non empty SubSpace of FT; :: thesis: for A being Subset of FT

for B being Subset of X9 st A = B holds

( A is connected iff B is connected )

let A8 be Subset of FT; :: thesis: for B being Subset of X9 st A8 = B holds

( A8 is connected iff B is connected )

let B8 be Subset of X9; :: thesis: ( A8 = B8 implies ( A8 is connected iff B8 is connected ) )

assume A1: A8 = B8 ; :: thesis: ( A8 is connected iff B8 is connected )

per cases
( A8 = {} or A8 <> {} )
;

end;

suppose A2:
A8 <> {}
; :: thesis: ( A8 is connected iff B8 is connected )

then reconsider A = A8 as non empty Subset of FT ;

reconsider B = B8 as non empty Subset of X9 by A1, A2;

reconsider X = X9 as non empty RelStr ;

end;reconsider B = B8 as non empty Subset of X9 by A1, A2;

reconsider X = X9 as non empty RelStr ;

A3: now :: thesis: ( not A8 is connected implies not B8 is connected )

assume
not A8 is connected
; :: thesis: not B8 is connected

then consider P, Q being Subset of FT such that

A4: A8 = P \/ Q and

A5: ( P <> {} & Q <> {} & P misses Q ) and

A6: P ^b misses Q ;

Q c= A8 by A4, XBOOLE_1:7;

then reconsider Q9 = Q as Subset of X by A1, XBOOLE_1:1;

P c= A8 by A4, XBOOLE_1:7;

then reconsider P9 = P as Subset of X by A1, XBOOLE_1:1;

A7: Q9 c= the carrier of X ;

P9 ^b = (P ^b) /\ ([#] X) by Th12;

then (P9 ^b) /\ Q9 = (P ^b) /\ (([#] X) /\ Q) by XBOOLE_1:16

.= (P ^b) /\ Q by A7, XBOOLE_1:28

.= {} by A6 ;

then P9 ^b misses Q9 ;

hence not B8 is connected by A1, A4, A5; :: thesis: verum

end;then consider P, Q being Subset of FT such that

A4: A8 = P \/ Q and

A5: ( P <> {} & Q <> {} & P misses Q ) and

A6: P ^b misses Q ;

Q c= A8 by A4, XBOOLE_1:7;

then reconsider Q9 = Q as Subset of X by A1, XBOOLE_1:1;

P c= A8 by A4, XBOOLE_1:7;

then reconsider P9 = P as Subset of X by A1, XBOOLE_1:1;

A7: Q9 c= the carrier of X ;

P9 ^b = (P ^b) /\ ([#] X) by Th12;

then (P9 ^b) /\ Q9 = (P ^b) /\ (([#] X) /\ Q) by XBOOLE_1:16

.= (P ^b) /\ Q by A7, XBOOLE_1:28

.= {} by A6 ;

then P9 ^b misses Q9 ;

hence not B8 is connected by A1, A4, A5; :: thesis: verum

now :: thesis: ( not B is connected implies not A is connected )

hence
( A8 is connected iff B8 is connected )
by A3; :: thesis: verumassume
not B is connected
; :: thesis: not A is connected

then consider P, Q being Subset of X9 such that

A8: ( B8 = P \/ Q & P <> {} & Q <> {} & P misses Q ) and

A9: P ^b misses Q ;

the carrier of X c= the carrier of FT by Def2;

then reconsider Q9 = Q as Subset of FT by XBOOLE_1:1;

the carrier of X c= the carrier of FT by Def2;

then reconsider P9 = P as Subset of FT by XBOOLE_1:1;

A10: P ^b = (P9 ^b) /\ ([#] X) by Th12;

(P9 ^b) /\ Q9 = (P9 ^b) /\ (([#] X) /\ Q) by XBOOLE_1:28

.= (P ^b) /\ Q by A10, XBOOLE_1:16

.= {} by A9 ;

then P9 ^b misses Q9 ;

hence not A is connected by A1, A8; :: thesis: verum

end;then consider P, Q being Subset of X9 such that

A8: ( B8 = P \/ Q & P <> {} & Q <> {} & P misses Q ) and

A9: P ^b misses Q ;

the carrier of X c= the carrier of FT by Def2;

then reconsider Q9 = Q as Subset of FT by XBOOLE_1:1;

the carrier of X c= the carrier of FT by Def2;

then reconsider P9 = P as Subset of FT by XBOOLE_1:1;

A10: P ^b = (P9 ^b) /\ ([#] X) by Th12;

(P9 ^b) /\ Q9 = (P9 ^b) /\ (([#] X) /\ Q) by XBOOLE_1:28

.= (P ^b) /\ Q by A10, XBOOLE_1:16

.= {} by A9 ;

then P9 ^b misses Q9 ;

hence not A is connected by A1, A8; :: thesis: verum