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 by A2;
hence T is connected ; :: thesis: verum