metamath/valid/mathd-algebra-101.mm

$(
  @{
    mathd-algebra-101.0 @e |- ( ph -> X e. RR ) $@
    mathd-algebra-101.1 @e |- ( ph -> ( ( ( X ^ 2 ) - ( 5 x. X ) ) - 4 ) <_ ; 1 0 ) $@
    @( (Contributed by Kunhao Zheng, 4-May-2021.) @)
    mathd-algebra-101 @p |- ( ph -> ( X >_ -u 2 /\ X <_ 7 ) ) @=
      ? @.
  @}
$)