let R be with_finite_stability# RelStr ; :: thesis:
let A be StableSet of R; :: thesis:
assume A1: card A = stability# R ; :: thesis:
set cP = the carrier of R;
the carrier of R c= (Upper A) \/ (Lower A)

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: x in the carrier of R ; :: thesis:
assume A3: not x in (Upper A) \/ (Lower A) ; :: thesis:
reconsider x = x as Element of the carrier of R by A2;
A4: not x in Upper A by A3, XBOOLE_0:def 3;
then A5: not x in A by XBOOLE_0:def 3;
A6: not x in uparrow A by A4, XBOOLE_0:def 3;
not x in Lower A by A3, XBOOLE_0:def 3;
then A7: not x in downarrow A by XBOOLE_0:def 3;
set Ax = A \/ {x};
A8: {x} c= the carrier of R by A2, ZFMISC_1:31;

let a, b be Element of R; :: thesis:
assume that
A9: a in A \/ {x} and
A10: b in A \/ {x} and
A11: a <> b ; :: thesis:

per cases by A9, A10, XBOOLE_0:def 3;

suppose ( a in A & b in A ) ; :: thesis:

hence ( not a <= b & not b <= a ) by A11, Def2; :: thesis:

end;

suppose A12: ( a in A & b in {x} ) ; :: thesis:

then b = x by TARSKI:def 1;
hence ( not a <= b & not b <= a ) by A6, A7, A12, WAYBEL_0:def 15, WAYBEL_0:def 16; :: thesis:

end;

suppose A13: ( a in {x} & b in A ) ; :: thesis:

then a = x by TARSKI:def 1;
hence ( not a <= b & not b <= a ) by A6, A7, A13, WAYBEL_0:def 15, WAYBEL_0:def 16; :: thesis:

end;

suppose ( a in {x} & b in {x} ) ; :: thesis:

then ( a = x & b = x ) by TARSKI:def 1;
hence ( not a <= b & not b <= a ) by A11; :: thesis:

end;

end;

end;

then A14: A \/ {x} is StableSet of R by A8, Def2, XBOOLE_1:8;
card (A \/ {x}) = (card A) + 1 by A5, CARD_2:41;
then card (A \/ {x}) > card A by NAT_1:13;
hence contradiction by Def6, A1, A14; :: thesis:

end;

hence (Upper A) \/ (Lower A) = [#] R ; :: thesis: