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, 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;

not [#] T is disconnected

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 not T is disconnected by Def3; :: thesis: verum