.....set predicate.....
IsRing(|<ℚ+*>|;+<ℚ+*>;0;-<ℚ+*>;*;1)
{ (RepUR ``ring_p`` 0 THEN Auto) }
IsGroup(ℚ;λx,y. (x + y);0;λx.-(x))
1. IsGroup(ℚ;λx,y. (x + y);0;λx.-(x))
⊢ IsMonoid(ℚ;λx,y. (x * y);1)
1. IsGroup(ℚ;λx,y. (x + y);0;λx.-(x))
2. IsMonoid(ℚ;λx,y. (x * y);1)
⊢ BiLinear(ℚ;λx,y. (x + y);λx,y. (x * y))