- R ≟ (mk_unary_morphism1 ??
- (λS:𝛀^AA.
- mk_unary_morphism1 ??
- (λS':𝛀^AA.
- mk_ext_powerclass AA (S - S') (ext_prop AA (substract_is_ext ? S S')))
- (prop11 ?? (substract_is_ext_morph AA S)))
- (prop11 ?? (substract_is_ext_morph AA))) ,
+ T ≟ ext_powerclass_setoid AA,
+ R ≟ mk_unary_morphism1 ?? (λX:𝛀^AA.
+ mk_unary_morphism1 ?? (λY:𝛀^AA.
+ mk_ext_powerclass AA
+ (ext_carr ? X - ext_carr ? Y)
+ (ext_prop AA (substract_is_ext ? X Y)))
+ (prop11 ?? (fun11 ?? (substract_is_ext_morph AA) X)))
+ (prop11 ?? (substract_is_ext_morph AA)),