let R be transitive RelStr ; :: thesis: for C being Clique of R
for x, y being Element of R st x is_minimal_in C & y <= x holds
C \/ {y} is Clique of R
let C be Clique of R; :: thesis: for x, y being Element of R st x is_minimal_in C & y <= x holds
C \/ {y} is Clique of R
let x, y be Element of R; :: thesis: ( x is_minimal_in C & y <= x implies C \/ {y} is Clique of R )
assume that
A1: x is_minimal_in C and
A2: y <= x ; :: thesis: C \/ {y} is Clique of R
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: ( not x in C \/ {y} or x in the carrier of R )
assume A6: x in C \/ {y} ; :: thesis: x in the carrier of R

per cases ( x in C or x in {y} ) by A6, XBOOLE_0:def 3;

suppose x in C ; :: thesis: x in the carrier of R

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

end;

suppose x in {y} ; :: thesis: x in the carrier of R

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

end;

end;

end;

now :: thesis: for a, b being Element of R st a in C \/ {y} & b in C \/ {y} & a <> b & not a <= b holds
b <= a

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

per cases ( ( a in C & b in C ) or ( a in C & b in {y} ) or ( a in {y} & b in C ) or ( a in {y} & b in {y} ) ) by A7, XBOOLE_0:def 3;

suppose ( a in C & b in C ) ; :: thesis: ( b₁ <= b₂ or b₂ <= b₁ )

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

end;

suppose that A9: a in C and
A10: b in {y} ; :: thesis: ( b₁ <= b₂ or b₂ <= b₁ )

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

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

suppose A13: a <> x ; :: thesis: ( b₁ <= b₂ or b₂ <= b₁ )

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: verum

end;

suppose x = a ; :: thesis: ( b₁ <= b₂ or b₂ <= b₁ )

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

end;

end;

end;

suppose that A14: a in {y} and
A15: b in C ; :: thesis: ( b₁ <= b₂ or b₂ <= b₁ )

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

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

suppose A18: b <> x ; :: thesis: ( b₁ <= b₂ or b₂ <= b₁ )

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: verum

end;

suppose x = b ; :: thesis: ( b₁ <= b₂ or b₂ <= b₁ )

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

end;

end;

end;

suppose ( a in {y} & b in {y} ) ; :: thesis: ( b₁ <= b₂ or b₂ <= b₁ )

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

end;

end;

end;

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