let T be non empty RelStr ; :: thesis: for a being set st [#] T = {a} holds
T is connected
let a be set ; :: thesis: ( [#] T = {a} implies T is connected )
reconsider OT = [#] T as non empty set ;
assume A1: [#] T = {a} ; :: thesis: T is connected
A2: for Z, Z9 being non empty Subset of OT holds not Z misses Z9

proof

let Z, Z9 be non empty Subset of OT; :: thesis: not Z misses Z9
Z = {a} by A1, ZFMISC_1:33;
hence not Z misses Z9 by A1, ZFMISC_1:33; :: thesis: verum

end;

[#] T is connected

proof

assume [#] T is disconnected ; :: thesis: contradiction
then ex A, B being Subset of T st
( A <> {} & B <> {} & [#] T = A \/ B & A misses B & the InternalRel of T = ( the InternalRel of T |_2 A) \/ ( the InternalRel of T |_2 B) ) by Def2;
hence contradiction by A2; :: thesis: verum

end;

hence T is connected by Def3; :: thesis: verum