let R be transitive antisymmetric with_finite_clique# RelStr ; :: thesis: Upper (minimals R) = [#] R
set ap = Upper (minimals R);
set cR = the carrier of R;
the carrier of R c= Upper (minimals R)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R or x in Upper (minimals R) )
assume A1: x in the carrier of R ; :: thesis: x in Upper (minimals R)
then reconsider x9 = x as Element of R ;
B1: not R is empty by A1;
then consider y being Element of R such that
C1: y is_minimal_in [#] R and
D1: ( y = x9 or y < x9 ) by Pmaxmin;
E1: y in minimals R by C1, B1, Lmin;

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

suppose x9 = y ; :: thesis: x in Upper (minimals R)

hence x in Upper (minimals R) by E1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose y < x9 ; :: thesis: x in Upper (minimals R)

then y <= x9 by ORDERS_2:def 10;
then x in uparrow (minimals R) by E1, WAYBEL_0:def 16;
hence x in Upper (minimals R) by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence Upper (minimals R) = [#] R by XBOOLE_0:def 10; :: thesis: verum