let S be Subset of R; :: thesis: ( S is trivial implies S is stable )
assume A1: S is trivial ; :: thesis: S is stable
let x, y be Element of R; :: according to DILWORTH:def 2 :: thesis: ( x in S & y in S & x <> y implies ( not x <= y & not y <= x ) )
thus ( x in S & y in S & x <> y implies ( not x <= y & not y <= x ) ) by A1, ZFMISC_1:def 10; :: thesis: verum