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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in maximals R )
assume A1: x in A ; :: thesis: x in maximals 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_maximal_in [#] R and
C1: ( y = x9 or x9 < y ) by A1a, Pminmax;
D1: ( y = x9 or x9 <= y ) by C1, ORDERS_2:def 10;
y in maximals R by A1a, B1, Lmax;
hence x in maximals R by A, A1, D1, LAChain; :: thesis: verum

end;

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