let R be non empty RelStr ; :: thesis: for a1, a2 being Element of R st ( a1 <= a2 or a2 <= a1 ) holds
{a1,a2} is Clique of R
let a1, a2 be Element of R; :: thesis: ( ( a1 <= a2 or a2 <= a1 ) implies {a1,a2} is Clique of R )
assume A1: ( a1 <= a2 or a2 <= a1 ) ; :: thesis: {a1,a2} is Clique of R
now :: thesis: for x, y being Element of R st x in {a1,a2} & y in {a1,a2} & x <> y & not x <= y holds
y <= x
let x, y be Element of R; :: thesis: ( x in {a1,a2} & y in {a1,a2} & x <> y & not x <= y implies y <= x )
assume ( x in {a1,a2} & y in {a1,a2} ) ; :: thesis: ( not x <> y or x <= y or y <= x )
then A2: ( ( x = a1 or x = a2 ) & ( y = a1 or y = a2 ) ) by TARSKI:def 2;
assume x <> y ; :: thesis: ( x <= y or y <= x )
hence ( x <= y or y <= x ) by A1, A2; :: thesis: verum
end;
hence {a1,a2} is Clique of R by Th6; :: thesis: verum