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 object ; :: 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 ;
A2: not P is empty by A1;
then consider y being Element of P such that
A3: y is_maximal_in [#] P and
A4: ( y = x9 or y > x9 ) by Th38;
A5: y in maximals P by A3, A2, Def10;

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

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

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

end;

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

then x9 <= y ;
then x in downarrow (maximals P) by A5, 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 ; :: thesis: verum