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
A: x is_maximal_in C and
B: x <= y ; :: thesis: C \/ {y} is Clique of R
C: x in C by A, WAYBEL_4:56;
B3a: not the carrier of R is empty by A, WAYBEL_4:56;
set Cb = C \/ {y};
D: C \/ {y} c= the carrier of R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in C \/ {y} or x in the carrier of R )
assume A1: x in C \/ {y} ; :: thesis: x in the carrier of R

per cases ( x in C or x in {y} ) by A1, 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 B3a; :: thesis: verum

end;

end;

end;

now

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
A3: ( a in C \/ {y} & b in C \/ {y} ) and
A3a: 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 A3, XBOOLE_0:def 3;

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

hence ( a <= b or b <= a ) by A3a, DClique; :: thesis: verum

end;

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

A4: b = y by T1, TARSKI:def 1;
B4: not x < a by A, S1, WAYBEL_4:56;

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

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

then ( a <= x or x <= a ) by S1, C, DClique;
hence ( a <= b or b <= a ) by B, A4, ORDERS_2:26, B4, ORDERS_2:def 10; :: thesis: verum

end;

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

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

end;

end;

end;

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

A4: a = y by S1, TARSKI:def 1;
B4: not x < b by A, T1, WAYBEL_4:56;

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

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

then ( b <= x or x <= b ) by T1, C, DClique;
hence ( a <= b or b <= a ) by B, A4, ORDERS_2:26, B4, ORDERS_2:def 10; :: thesis: verum

end;

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

hence ( a <= b or b <= a ) by B, S1, 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 A3a; :: thesis: verum

end;

end;

end;

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