let R be transitive antisymmetric with_finite_clique# RelStr ; :: thesis: for A being StableSet of R st minimals R c= A holds
A = minimals R
let A be StableSet of R; :: thesis: ( minimals R c= A implies A = minimals R )
assume A: minimals R c= A ; :: thesis: A = minimals R
A c= minimals R

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in minimals R )
assume A1: x in A ; :: thesis: x in minimals R
then A1a: not R is empty ;
reconsider x9 = x as Element of R by A1;
consider y being Element of R such that
B1: y is_minimal_in [#] R and
C1: ( y = x9 or y < x9 ) by A1a, Pmaxmin;
D1: ( y = x9 or y <= x9 ) by C1, ORDERS_2:def 10;
y in minimals R by A1a, B1, Lmin;
hence x in minimals R by A, A1, D1, LAChain; :: thesis: verum

end;

hence A = minimals R by A, XBOOLE_0:def 10; :: thesis: verum