let R be transitive antisymmetric RelStr ; 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; for z being set st z in Upper A & z in Lower A holds
z in A
let z be set ; ( 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
; z in A
per cases
( z in A or not z in A )
;
suppose A3:
not
z in A
;
z in Athen 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;
verum end;