let R be SimpleGraph; :: 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
set VR = Vertices R;
reconsider BB = B as Subset of (Vertices R) by XBOOLE_1:1;
BB is stable

proof

let x, y be set ; :: according to SCMYCIEL:def 19 :: thesis: ( x <> y & x in BB & y in BB implies {x,y} nin R )
assume A1: ( x <> y & x in BB & y in BB ) ; :: thesis: {x,y} nin R
thus {x,y} nin R by A1, Lstable; :: thesis: verum

end;

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