let P be transitive antisymmetric with_finite_clique# RelStr ; :: thesis: Lower (maximals P) = [#] P
set ap = Lower (maximals P);
set cP = the carrier of P;
the carrier of P c= Lower (maximals P)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of P or x in Lower (maximals P) )
assume A1: x in the carrier of P ; :: thesis: x in Lower (maximals P)
then reconsider x' = x as Element of ;
B1: not P is empty by A1;
consider y being Element of such that
C1: y is_maximal_in [#] P and
D1: ( y = x' or y > x' ) by B1, Pminmax;
E1: y in maximals P by C1, B1, Lmax;

per cases ( x' = y or y > x' ) by D1;

suppose x' = y ; :: thesis: x in Lower (maximals P)

hence x in Lower (maximals P) by E1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose y > x' ; :: thesis: x in Lower (maximals P)

then x' <= y by ORDERS_2:def 10;
then x in downarrow (maximals P) by E1, WAYBEL_0:def 15;
hence x in Lower (maximals P) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence Lower (maximals P) = [#] P by XBOOLE_0:def 10; :: thesis: verum