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 A1: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R or x in (Upper A) \/ (Lower A) )
assume A2: x in the carrier of R ; :: thesis: x in (Upper A) \/ (Lower A)
assume A3: not x in (Upper A) \/ (Lower A) ; :: thesis: contradiction
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;

now :: thesis: for a, b being Element of R st a in A \/ {x} & b in A \/ {x} & a <> b holds
( not a <= b & not b <= a )

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
A9: a in A \/ {x} and
A10: b in A \/ {x} and
A11: 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 A9, A10, 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 A11, Def2; :: thesis: verum

end;

suppose A12: ( 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 A6, A7, A12, WAYBEL_0:def 15, WAYBEL_0:def 16; :: thesis: verum

end;

suppose A13: ( 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 A6, A7, A13, WAYBEL_0:def 15, WAYBEL_0:def 16; :: 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 A11; :: thesis: verum

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: verum

end;

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