let R be transitive RelStr ; :: thesis:
let C be Clique of R; :: thesis:
let x, y be Element of R; :: thesis:
assume that
A1: x is_minimal_in C and
A2: y <= x ; :: thesis:
A3: x in C by A1, WAYBEL_4:56;
A4: not the carrier of R is empty by A1, WAYBEL_4:56;
set Cb = C \/ {y};
A5: C \/ {y} c= the carrier of R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: x in C \/ {y} ; :: thesis:

per cases by A6, XBOOLE_0:def 3;

suppose x in C ; :: thesis:

hence x in the carrier of R ; :: thesis:

end;

suppose x in {y} ; :: thesis:

then x = y by TARSKI:def 1;
hence x in the carrier of R by A4; :: thesis:

end;

end;

end;

now :: thesis:

let a, b be Element of R; :: thesis:
assume that
A7: ( a in C \/ {y} & b in C \/ {y} ) and
A8: a <> b ; :: thesis:

per cases by A7, XBOOLE_0:def 3;

suppose ( a in C & b in C ) ; :: thesis:

hence ( a <= b or b <= a ) by A8, Th6; :: thesis:

end;

suppose that A9: a in C and
A10: b in {y} ; :: thesis:

A11: b = y by A10, TARSKI:def 1;
A12: not a < x by A1, A9, WAYBEL_4:56;

per cases ;

suppose A13: a <> x ; :: thesis:

then not a <= x by A12;
then x <= a by A9, A3, A13, Th6;
hence ( a <= b or b <= a ) by A2, A11, ORDERS_2:3; :: thesis:

end;

suppose x = a ; :: thesis:

hence ( a <= b or b <= a ) by A2, A10, TARSKI:def 1; :: thesis:

end;

end;

end;

suppose that A14: a in {y} and
A15: b in C ; :: thesis:

A16: a = y by A14, TARSKI:def 1;
A17: not b < x by A1, A15, WAYBEL_4:56;

per cases ;

suppose A18: b <> x ; :: thesis:

then not b <= x by A17;
then x <= b by A15, A3, A18, Th6;
hence ( a <= b or b <= a ) by A2, A16, ORDERS_2:3; :: thesis:

end;

suppose x = b ; :: thesis:

hence ( a <= b or b <= a ) by A2, A14, TARSKI:def 1; :: thesis:

end;

end;

end;

suppose ( a in {y} & b in {y} ) ; :: thesis:

then ( a = y & b = y ) by TARSKI:def 1;
hence ( a <= b or b <= a ) by A8; :: thesis:

end;

end;

end;

hence C \/ {y} is Clique of R by A5, Th6; :: thesis: