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 A1: not maximals R c= A ; :: thesis: not maximals R c= Lower A
consider x being object such that
A2: x in maximals R and
A3: not x in A by A1;
assume A4: maximals R c= Lower A ; :: thesis: contradiction
reconsider x9 = x as Element of R by A2;
not R is empty by A2;
then A5: x9 is_maximal_in [#] R by A2, Def10;
x9 in downarrow A by A3, A2, A4, XBOOLE_0:def 3;
then consider x99 being Element of R such that
A6: x9 <= x99 and
A7: x99 in A by WAYBEL_0:def 15;
now :: thesis: not x99 <> x9
assume x99 <> x9 ; :: thesis: contradiction
then x9 < x99 by A6;
hence contradiction by A2, A5, WAYBEL_4:55; :: thesis: verum
end;
hence contradiction by A7, A3; :: thesis: verum