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 A1: not R is empty ; :: thesis: A is StableSet of R
per cases ( S is empty or not S is empty ) ;
suppose A2: 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
A3: x in A and
A4: y in A and
A5: x <> y ; :: thesis: ( not x <= y & not y <= x )
reconsider x9 = x, y9 = y as Element of (subrelstr S) by A3, A4;
( not x9 <= y9 & not y9 <= x9 ) by A3, A4, A5, Def2;
hence ( not x <= y & not y <= x ) by A1, A2, YELLOW_0:60; :: thesis: verum
end;
hence A is StableSet of R ; :: thesis: verum
end;
end;
end;
end;