let R be transitive RelStr ; :: thesis: for C being Clique of R
for x, y being Element of R st x is_maximal_in C & x <= y holds
C \/ {y} is Clique of R
let C be Clique of R; :: thesis: for x, y being Element of R st x is_maximal_in C & x <= y holds
C \/ {y} is Clique of R
let x, y be Element of R; :: thesis: ( x is_maximal_in C & x <= y implies C \/ {y} is Clique of R )
assume that
A1: x is_maximal_in C and
A2: x <= y ; :: thesis: C \/ {y} is Clique of R
A3: x in C by A1, WAYBEL_4:55;
A4: not the carrier of R is empty by A1, WAYBEL_4:55;
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 x < a by A1, A9, WAYBEL_4:55;

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

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

then ( a <= x or x <= a ) by A9, A3, Th6;
hence ( a <= b or b <= a ) by A2, A11, A12, 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 A13: a in {y} and
A14: b in C ; :: thesis: ( b₁ <= b₂ or b₂ <= b₁ )

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

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

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

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

end;

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

hence ( a <= b or b <= a ) by A2, A13, 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