let R be transitive RelStr ; :: thesis: for A being StableSet of R
for C being Clique of (subrelstr (Upper A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
a <= b
let A be StableSet of R; :: thesis: for C being Clique of (subrelstr (Upper A))
for a, b being Element of R st a in A & a in C & b in C & not a = b holds
a <= b
let C be Clique of (subrelstr (Upper A)); :: thesis: for a, b being Element of R st a in A & a in C & b in C & not a = b holds
a <= b
let a, b be Element of R; :: thesis: ( a in A & a in C & b in C & not a = b implies a <= b )
assume that
A1: a in A and
A2: a in C and
A3: b in C ; :: thesis: ( a = b or a <= b )
set ap = subrelstr (Upper A);
reconsider a9 = a as Element of (subrelstr (Upper A)) by A2;
A4: b in the carrier of (subrelstr (Upper A)) by A3;
reconsider b9 = b as Element of (subrelstr (Upper A)) by A3;
A5: b9 in Upper A by A4, YELLOW_0:def 15;
A6: C is Clique of R by Th28;
per cases ( b9 in A or b9 in uparrow A ) by A5, XBOOLE_0:def 3;
suppose b9 in A ; :: thesis: ( a = b or a <= b )
hence ( a = b or a <= b ) by A1, A2, A3, A6, Th15; :: thesis: verum
end;
suppose b9 in uparrow A ; :: thesis: ( a = b or a <= b )
then consider c being Element of R such that
A7: c <= b and
A8: c in A by WAYBEL_0:def 16;
per cases ( a <> b or a = b ) ;
suppose A9: a <> b ; :: thesis: ( a = b or a <= b )
per cases ( a9 <= b9 or b9 <= a9 ) by A9, A2, A3, Th6;
suppose a9 <= b9 ; :: thesis: ( a = b or a <= b )
hence ( a = b or a <= b ) by YELLOW_0:59; :: thesis: verum
end;
suppose b9 <= a9 ; :: thesis: ( a = b or a <= b )
then b <= a by YELLOW_0:59;
then c <= a by A7, YELLOW_0:def 2;
hence ( a = b or a <= b ) by A8, A7, A1, Def2; :: thesis: verum
end;
end;
end;
suppose a = b ; :: thesis: ( a = b or a <= b )
hence ( a = b or a <= b ) ; :: thesis: verum
end;
end;
end;
end;