let R be transitive antisymmetric RelStr ; :: thesis: for A being StableSet of R
for z being set st z in Upper A & z in Lower A holds
z in A
let A be StableSet of R; :: thesis: for z being set st z in Upper A & z in Lower A holds
z in A
let z be set ; :: thesis: ( z in Upper A & z in Lower A implies z in A )
assume that
A: z in Upper A and
B: z in Lower A ; :: thesis: z in A

per cases ( z in A or not z in A ) ;

suppose z in A ; :: thesis: z in A

hence z in A ; :: thesis: verum

end;

suppose S1: not z in A ; :: thesis: z in A

then A1: z in uparrow A by A, XBOOLE_0:def 3;
B1: z in downarrow A by B, S1, XBOOLE_0:def 3;
reconsider y = z as Element of R by A;
consider x being Element of R such that
E: x <= y and
F: x in A by A1, WAYBEL_0:def 16;
reconsider x9 = z as Element of R by B;
consider y9 being Element of R such that
I: x9 <= y9 and
J: y9 in A by B1, WAYBEL_0:def 15;
x <= y9 by E, I, YELLOW_0:def 2;
then x = y9 by F, J, LAChain;
hence z in A by E, F, I, YELLOW_0:def 3; :: thesis: verum

end;

end;