\forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (\forall
(i: nat).(\forall (b2: A).((aprem i a2 b2) \to (ex2 A (\lambda (b1: A).(leq g
b1 b2)) (\lambda (b1: A).(aprem i a1 b1)))))))))
\forall (g: G).(\forall (a1: A).(\forall (a2: A).((leq g a1 a2) \to (\forall
(i: nat).(\forall (b2: A).((aprem i a2 b2) \to (ex2 A (\lambda (b1: A).(leq g
b1 b2)) (\lambda (b1: A).(aprem i a1 b1)))))))))