let R be transitive RelStr ; :: thesis: for A being StableSet of R
for C being Clique of (subrelstr (Lower A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
b <= a
let A be StableSet of R; :: thesis: for C being Clique of (subrelstr (Lower A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
b <= a
let C be Clique of (subrelstr (Lower A)); :: thesis: for a, b being Element of R st a in A & a in C & b in C & not a = b holds
b <= a
let a, b be Element of R; :: thesis: ( a in A & a in C & b in C & not a = b implies b <= a )
assume that
A: a in A and
B: a in C and
C: b in C ; :: thesis: ( a = b or b <= a )
set ap = subrelstr (Lower A);
reconsider a9 = a as Element of (subrelstr (Lower A)) by B;
Da: b in the carrier of (subrelstr (Lower A)) by C;
reconsider b9 = b as Element of (subrelstr (Lower A)) by C;
D: b9 in Lower A by Da, YELLOW_0:def 15;
E: C is Clique of R by SPClique;

per cases ( b9 in A or b9 in downarrow A ) by D, XBOOLE_0:def 3;

suppose b9 in A ; :: thesis: ( a = b or b <= a )

hence ( a = b or b <= a ) by A, B, C, E, ACClique; :: thesis: verum

end;

suppose b9 in downarrow A ; :: thesis: ( a = b or b <= a )

then consider c being Element of R such that
A1: b <= c and
B1: c in A by WAYBEL_0:def 15;

per cases ( a <> b or a = b ) ;

suppose Ax: a <> b ; :: thesis: ( a = b or b <= a )

per cases ( a9 <= b9 or b9 <= a9 ) by Ax, B, C, DClique;

suppose a9 <= b9 ; :: thesis: ( a = b or b <= a )

then a <= b by YELLOW_0:60;
then a <= c by A1, YELLOW_0:def 2;
hence ( a = b or b <= a ) by B1, A1, A, LAChain; :: thesis: verum

end;

suppose b9 <= a9 ; :: thesis: ( a = b or b <= a )

hence ( a = b or b <= a ) by YELLOW_0:60; :: thesis: verum

end;

end;

end;

suppose a = b ; :: thesis: ( a = b or b <= a )

hence ( a = b or b <= a ) ; :: thesis: verum

end;

end;

end;

end;