let a, b be Element of R; :: thesis: ( a in C & b in C & a <> b & not a <= b implies b <= a )
assume that
A2: a in C and
A3: b in C and
A4: 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
A5: 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 A1;
consider c being set such that
A6: c in P and
A7: S /\ C c= c and
for d being set st d in P & d <> c holds
C /\ d = {} by A5;
c is Clique of (subrelstr S) by A6, Def11;
then A8: c is Clique of R by Th28;
( a in S & b in S ) by TARSKI:def 2;
then ( a in S /\ C & b in S /\ C ) by A2, A3, XBOOLE_0:def 4;
hence ( a <= b or b <= a ) by A7, A8, A4, Th6; :: thesis: verum