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

now

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

end;

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