let R be RelStr ; :: thesis: for A being StableSet of R st not minimals R c= A holds
not minimals R c= Upper A
let A be StableSet of R; :: thesis: ( not minimals R c= A implies not minimals R c= Upper A )
assume not minimals R c= A ; :: thesis: not minimals R c= Upper A
then consider x being set such that
B: x in minimals R and
C: not x in A by TARSKI:def 3;
assume D: minimals R c= Upper A ; :: thesis: contradiction
reconsider x9 = x as Element of R by B;
not R is empty by B;
then B1: x9 is_minimal_in [#] R by B, Lmin;
x9 in uparrow A by C, B, D, XBOOLE_0:def 3;
then consider x99 being Element of R such that
C1: x99 <= x9 and
D1: x99 in A by WAYBEL_0:def 16;

now

assume x99 <> x9 ; :: thesis: contradiction
then x99 < x9 by C1, ORDERS_2:def 10;
hence contradiction by B, B1, WAYBEL_4:57; :: thesis: verum

end;

hence contradiction by D1, C; :: thesis: verum