let R be RelStr ; :: thesis: for A being StableSet of R
for B being Subset of A holds B is StableSet of R
let A be StableSet of R; :: thesis: for B being Subset of A holds B is StableSet of R
let B be Subset of A; :: thesis: B is StableSet of R
reconsider BB = B as Subset of R by XBOOLE_1:1;
BB is stable

proof

let x, y be Element of R; :: according to DILWORTH:def 2 :: thesis: ( x in BB & y in BB & x <> y implies ( not x <= y & not y <= x ) )
assume A1: ( x in BB & y in BB & x <> y ) ; :: thesis: ( not x <= y & not y <= x )
thus ( not x <= y & not y <= x ) by A1, Def2; :: thesis: verum

end;

hence B is StableSet of R ; :: thesis: verum