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