let R be RelStr ; :: thesis: for S being Subset of R
for A being StableSet of (subrelstr S) holds A is StableSet of R
let S be Subset of R; :: thesis: for A being StableSet of (subrelstr S) holds A is StableSet of R
let A be StableSet of (subrelstr S); :: thesis: A is StableSet of R
set sS = subrelstr S;

per cases ( R is empty or not R is empty ) ;

suppose R is empty ; :: thesis: A is StableSet of R

then the carrier of (subrelstr S) = {} by YELLOW_0:def 15;
then A = {} R ;
hence A is StableSet of R ; :: thesis: verum

end;

suppose S1: not R is empty ; :: thesis: A is StableSet of R

per cases ( S is empty or not S is empty ) ;

suppose S is empty ; :: thesis: A is StableSet of R

then the carrier of (subrelstr S) = {} by YELLOW_0:def 15;
then A = {} R ;
hence A is StableSet of R ; :: thesis: verum

end;

suppose S2: not S is empty ; :: thesis: A is StableSet of R

S = the carrier of (subrelstr S) by YELLOW_0:def 15;
then reconsider A = A as Subset of R by XBOOLE_1:1;
A is stable

proof

let x, y be Element of R; :: according to DILWORTH:def 2 :: thesis: ( x in A & y in A & x <> y implies ( not x <= y & not y <= x ) )
assume that
A1: x in A and
B1: y in A and
C1: x <> y ; :: thesis: ( not x <= y & not y <= x )
reconsider x9 = x, y9 = y as Element of (subrelstr S) by A1, B1;
( not x9 <= y9 & not y9 <= x9 ) by A1, B1, C1, LAChain;
hence ( not x <= y & not y <= x ) by S1, S2, YELLOW_0:61; :: thesis: verum

end;

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

end;

end;

end;

end;