Properties in Redefinitions

Properties - Predicates

reflexivity
definition
  let X, Y be set;
  redefine pred X c= Y;
  reflexivity
  proof
    thus for x being set holds x c= x;
  end;
end;
irreflexivity
definition
  let X, Y be set;
  redefine pred X c= Y;
  irreflexivity
  proof
    thus for x being set holds not x c= x;
  end;
end;
symmetry
definition
  let X, Y be set;
  redefine pred X c= Y;
  symmetry
  proof
    thus for x, y being set st x c= y holds y c= x;
  end;
end;
asymmetry
definition
  let X, Y be set;
  redefine pred X c= Y;
  asymmetry
  proof
    thus for x, y being set st x c= y holds not y c= x;
  end;
end;
connectedness
definition
  let X, Y be set;
  redefine pred X c= Y;
  connectedness
  proof
    thus for x, y being set holds x c= y or y c= x;
  end;
end;

Properties - Functors

commutativity
definition
  let X, Y be set;
  redefine func X + Y;
  commutativity
  proof
    thus for x, y being set holds x + y = y + x;
  end;
end;