let R be non empty RelStr ; :: thesis: for a1, a2 being Element of R holds
( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R )
let a1, a2 be Element of R; :: thesis: ( a1 <= a2 or a2 <= a1 or {a1,a2} is StableSet of R )
assume A1: ( not a1 <= a2 & not a2 <= a1 ) ; :: thesis: {a1,a2} is StableSet of R
set S = {a1,a2};
{a1,a2} is stable
proof
let x, y be Element of R; :: according to DILWORTH:def 2 :: thesis: ( x in {a1,a2} & y in {a1,a2} & x <> y implies ( not x <= y & not y <= x ) )
assume A2: ( x in {a1,a2} & y in {a1,a2} & x <> y ) ; :: thesis: ( not x <= y & not y <= x )
( ( x = a1 or x = a2 ) & ( y = a1 or y = a2 ) ) by A2, TARSKI:def 2;
hence ( not x <= y & not y <= x ) by A1, A2; :: thesis: verum
end;
hence {a1,a2} is StableSet of R ; :: thesis: verum