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