[mizar] Element versus Subgroup

[Freek Wiedijk <freek@cs.ru.nl>]

Dear all,

If I do

	reserve G for Group;
	reserve H for Subgroup of G;
	reserve h for Element of H;

(like in GROUP_2, for example), I don't think I can make

	h qua Element of G

work.  I think one would have to redefine the type of a
field in a structure, or something like that, and I don't
see how to do that.

So are these thoughts correct?

And if one would do structures in the Lee/Rudnicki way,
would this be different?

Freek