let C be Subset of R; :: thesis: ( C is strong-chain implies C is connected )
assume A: C is strong-chain ; :: thesis: C is connected

now

let a, b be Element of R; :: thesis: ( a in C & b in C & a <> b & not a <= b implies b <= a )
assume that
A1: a in C and
B1: b in C and
B1a: a <> b ; :: thesis: ( a <= b or b <= a )
set S = {a,b};
reconsider S = {a,b} as non empty finite Subset of R ;
consider P being Clique-partition of (subrelstr S) such that
card P <= stability# R and
C1: ex c being set st
( c in P & S /\ C c= c & ( for d being set st d in P & d <> c holds
C /\ d = {} ) ) by A, Lsc;
consider c being set such that
D1: c in P and
E1: S /\ C c= c and
for d being set st d in P & d <> c holds
C /\ d = {} by C1;
c is Clique of (subrelstr S) by D1, LCpart;
then F1: c is Clique of R by SPClique;
( a in S & b in S ) by TARSKI:def 2;
then ( a in S /\ C & b in S /\ C ) by A1, B1, XBOOLE_0:def 4;
hence ( a <= b or b <= a ) by E1, F1, B1a, DClique; :: thesis: verum

end;

hence C is connected by DClique; :: thesis: verum