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 object such that
A1: x in minimals R and
A2: not x in A ;
assume A3: minimals R c= Upper A ; :: thesis: contradiction
reconsider x9 = x as Element of R by A1;
not R is empty by A1;
then A4: x9 is_minimal_in [#] R by A1, Def9;
x9 in uparrow A by A2, A1, A3, XBOOLE_0:def 3;
then consider x99 being Element of R such that
A5: x99 <= x9 and
A6: x99 in A by WAYBEL_0:def 16;

now :: thesis: not x99 <> x9

assume x99 <> x9 ; :: thesis: contradiction
then x99 < x9 by A5;
hence contradiction by A1, A4, WAYBEL_4:56; :: thesis: verum

end;

hence contradiction by A6, A2; :: thesis: verum