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 x9 = x as Element of P ;
B1: not P is empty by A1;
then consider y being Element of P such that
C1: y is_maximal_in [#] P and
D1: ( y = x9 or y > x9 ) by Pminmax;
E1: y in maximals P by C1, B1, Lmax;

per cases ( x9 = y or y > x9 ) by D1;

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

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

end;

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

then x9 <= 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