6.6 Mode Definition

At last, we will explain the mode definition.
    Let us assume that we will newly define a mode nlt2_elements.

      definition
        mode nlt2_elements　->　set means
        :DF2:
        ex a,b st a in it & b in it & a <> b;
         existence
         proof
           take B = NAT;
           thus ex a,b st a in B & b in B & a <> b
             proof
               take a= 1, b = 2;
               thus a in B & b in B & a <> b;
             end;
         end;
      end;


In the demonstration section of the mode definition, only the demonstration of existence will be needed. Also, when the mode is defined, its natural property can be defined by (attribute) or (cluster). For instance:

      definition
      attr nlt2_elements -> set means :DF2:
      ex a,b st a in it & b in it & a <> b;
      end;
      definition
      cluster nlt2_elements set;
      existence
      proof
        take B=NAT;
        ex a,b st a in B & b in B & a <> b
        proof
          take a=1, b=2;
          thus a in B & b in B & a <> b;
        end;
     hence thesis by DF2;
     end;
     end;

Generally, attribute takes the following predicate form:

    A is non-empty

Or, the adjective form.

    non-empty set

In this case, non-empty is the same with non empty.
Also, in the definition blocks of attribute, we can define symbols that possess the same meaning (synonym) and the opposite meaning(antonym).

Example (this is not actual)

    definition
      attr empty -&gt　set means :A1:
       not ex x st x∈it;
       ...
      synonym (void);
      antonym (non-empty);
    end;

When we want to use by attaching multiple attributes to one mode, that cluster needs to be defined. If this is not done, the following inconsistent combination will appear.

    finite infinite set
    empty non-empty set

As it has been stated before, new functor, mode, attribute, cluster (cf. §6.7), and others can be defined in Mizar; however, each demonstration needs to include the following elements.