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

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

suppose R is empty ; :: thesis: A /\ S is StableSet of (subrelstr S)

then A /\ S = {} (subrelstr S) ;
hence A /\ S is StableSet of (subrelstr S) ; :: thesis: verum

end;

suppose S1: not R is empty ; :: thesis: A /\ S is StableSet of (subrelstr S)

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

suppose S is empty ; :: thesis: A /\ S is StableSet of (subrelstr S)

then A /\ S = {} (subrelstr S) ;
hence A /\ S is StableSet of (subrelstr S) ; :: thesis: verum

end;

suppose S2: not S is empty ; :: thesis: A /\ S is StableSet of (subrelstr S)

S = the carrier of (subrelstr S) by YELLOW_0:def 15;
then reconsider AS = A /\ S as Subset of (subrelstr S) by XBOOLE_1:17;
AS is stable

proof

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

end;

hence A /\ S is StableSet of (subrelstr S) ; :: thesis: verum

end;

end;

end;

end;