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 S1:
not
z in A
;
:: thesis: z in AA1:
z in uparrow A
by A, S1, 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 x' =
z as
Element of
R by B;
consider y' being
Element of
R such that I:
x' <= y'
and J:
y' in A
by B1, WAYBEL_0:def 15;
x <= y'
by E, I, YELLOW_0:def 2;
then
x = y'
by F, J, LAChain;
hence
z in A
by E, F, I, YELLOW_0:def 3;
:: thesis: verum end;