let R be with_finite_stability# RelStr ; :: thesis: for A being StableSet of R st card A = stability# R holds
(Upper A) \/ (Lower A) = [#] R
let A be StableSet of R; :: thesis: ( card A = stability# R implies (Upper A) \/ (Lower A) = [#] R )
assume AA: card A = stability# R ; :: thesis: (Upper A) \/ (Lower A) = [#] R
set cP = the carrier of R;
the carrier of R c= (Upper A) \/ (Lower A)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R or x in (Upper A) \/ (Lower A) )
assume A: x in the carrier of R ; :: thesis: x in (Upper A) \/ (Lower A)
assume B: not x in (Upper A) \/ (Lower A) ; :: thesis: contradiction
reconsider x = x as Element of the carrier of R by A;
C: not x in Upper A by B, XBOOLE_0:def 3;
Ca: not x in A by C, XBOOLE_0:def 3;
Cb: not x in uparrow A by C, XBOOLE_0:def 3;
D: not x in Lower A by B, XBOOLE_0:def 3;
Db: not x in downarrow A by D, XBOOLE_0:def 3;
set Ax = A \/ {x};
Ka: {x} c= the carrier of R by A, ZFMISC_1:37;

now

let a, b be Element of R; :: thesis: ( a in A \/ {x} & b in A \/ {x} & a <> b implies ( not b₁ <= b₂ & not b₂ <= b₁ ) )
assume that
A1: a in A \/ {x} and
B1: b in A \/ {x} and
C1: a <> b ; :: thesis: ( not b₁ <= b₂ & not b₂ <= b₁ )

per cases ( ( a in A & b in A ) or ( a in A & b in {x} ) or ( a in {x} & b in A ) or ( a in {x} & b in {x} ) ) by A1, B1, XBOOLE_0:def 3;

suppose ( a in A & b in A ) ; :: thesis: ( not b₁ <= b₂ & not b₂ <= b₁ )

hence ( not a <= b & not b <= a ) by C1, LAChain; :: thesis: verum

end;

suppose S1: ( a in A & b in {x} ) ; :: thesis: ( not b₁ <= b₂ & not b₂ <= b₁ )

then b = x by TARSKI:def 1;
hence ( not a <= b & not b <= a ) by Cb, WAYBEL_0:def 16, Db, WAYBEL_0:def 15, S1; :: thesis: verum

end;

suppose S1: ( a in {x} & b in A ) ; :: thesis: ( not b₁ <= b₂ & not b₂ <= b₁ )

then a = x by TARSKI:def 1;
hence ( not a <= b & not b <= a ) by Cb, WAYBEL_0:def 16, Db, WAYBEL_0:def 15, S1; :: thesis: verum

end;

suppose ( a in {x} & b in {x} ) ; :: thesis: ( not b₁ <= b₂ & not b₂ <= b₁ )

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

end;

end;

end;

then P: A \/ {x} is StableSet of R by Ka, XBOOLE_1:8, LAChain;
card (A \/ {x}) = (card A) + 1 by Ca, CARD_2:54;
then card (A \/ {x}) > card A by NAT_1:13;
hence contradiction by Lwidth, AA, P; :: thesis: verum

end;

hence (Upper A) \/ (Lower A) = [#] R by XBOOLE_0:def 10; :: thesis: verum