set R = the connected Order of X;
take the connected Order of X ; :: thesis: the connected Order of X is connected
thus the connected Order of X is connected ; :: thesis: verum