theorem :: ANPROJ_8:87

( <*<e1>*> @ = F2M <e1> & <*<e2>*> @ = F2M <e2> & <*<e3>*> @ = F2M <e3> )