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
A1: z in Upper A and
A2: 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 A3: not z in A ; :: thesis: z in A

then A4: z in uparrow A by A1, XBOOLE_0:def 3;
A5: z in downarrow A by A2, A3, XBOOLE_0:def 3;
reconsider y = z as Element of R by A1;
consider x being Element of R such that
A6: x <= y and
A7: x in A by A4, WAYBEL_0:def 16;
reconsider x9 = z as Element of R by A2;
consider y9 being Element of R such that
A8: x9 <= y9 and
A9: y9 in A by A5, WAYBEL_0:def 15;
x <= y9 by A6, A8, YELLOW_0:def 2;
then x = y9 by A7, A9, Def2;
hence z in A by A6, A7, A8, YELLOW_0:def 3; :: thesis: verum

end;

end;