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 A1: maximals R c= A ; :: thesis: A = maximals R
A c= maximals R
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in maximals R )
assume A2: x in A ; :: thesis: x in maximals 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_maximal_in [#] R and
A5: ( y = x9 or x9 < y ) by A3, Th38;
A6: ( y = x9 or x9 <= y ) by A5;
y in maximals R by A3, A4, Def10;
hence x in maximals R by A1, A2, A6, Def2; :: thesis: verum
end;
hence A = maximals R by A1; :: thesis: verum