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

proof

let Z, Z' be non empty Subset of OT; :: thesis: not Z misses Z'
( Z = {a} & Z' = {a} ) by A1, ZFMISC_1:39;
hence not Z misses Z' ; :: thesis: verum

end;

not [#] T is disconnected

proof

assume [#] T is disconnected ; :: thesis: contradiction
then consider A, B being Subset of T such that
A3: ( 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;
thus contradiction by A2, A3; :: thesis: verum

end;

hence not T is disconnected by Def3; :: thesis: verum