object Being;

    op Jx(Being)->boolean;
        (* Return true if the given being is a judge *)

    op Lx(Being)->boolean;
        (* Return true if the given being is a lawyer *)

    axiom G = forall (x:Being | Lx(x)) Jx(x);
        (* Transliteration of Gries' forall x | Lx : Jx *)


    (* Alternative formulation (pretty lame, actually) *)
    var Lx_v,Jx_v: boolean;

    axiom LJ = Lx_v = Jx_v;