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 A1: minimals R c= A ; :: thesis: A = minimals R
A c= minimals R

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in minimals R )
assume A2: x in A ; :: thesis: x in minimals R
then A3: not R is empty ;
reconsider x9 = x as Element of R by A2;
consider y being Element of R such that
A4: y is_minimal_in [#] R and
A5: ( y = x9 or y < x9 ) by A3, Th36;
A6: ( y = x9 or y <= x9 ) by A5;
y in minimals R by A3, A4, Def9;
hence x in minimals R by A1, A2, A6, Def2; :: thesis: verum

end;

hence A = minimals R by A1; :: thesis: verum