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 )
reconsider OT = [#] T as non empty set ;
assume A1: [#] T = {a} ; :: thesis: not T is disconnected
A2: for Z, Z' being non empty Subset of holds not Z misses Z'

proof

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

end;

not [#] T is disconnected

proof

assume [#] T is disconnected ; :: thesis: contradiction
then ex A, B being Subset of 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 not T is disconnected by Def3; :: thesis: verum