Intuitionize dftpos3 in iset.mm
Intuitionize dftpos3 in iset.mm

Change brtpos to brtposg . Fortunately, the additional conditions
are trivially satisfied.

metamath/set.mm,metamath/set.mm,metamath/set.mm