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 object ; :: 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 ;
A2: not R is empty by A1;
then consider y being Element of R such that
A3: y is_minimal_in [#] R and
A4: ( y = x9 or y < x9 ) by Th36;
A5: y in minimals R by A3, A2, Def9;

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

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

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

end;

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

then y <= x9 ;
then x in uparrow (minimals R) by A5, 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 ; :: thesis: verum