const In : set set prop term iIn = In infix iIn 2000 2000 term In_rec_G_iii = \P:set (set set set set) set set set.\x:set.\g:set set set.!Q:set (set set set) prop.(!y:set.!R:set set set set.(!z:set.z iIn y -> Q z (R z)) -> Q y (P y R)) -> Q x g const In_rec_iii : (set (set set set set) set set set) set set set set axiom In_rec_G_iii_In_rec_iii: !P:set (set set set set) set set set.(!x:set.!Q:set set set set.!R:set set set set.(!y:set.y iIn x -> Q y = R y) -> P x Q = P x R) -> !x:set.In_rec_G_iii P x (In_rec_iii P x) claim !P:set (set set set set) set set set.(!x:set.!Q:set set set set.!R:set set set set.(!y:set.y iIn x -> Q y = R y) -> P x Q = P x R) -> !x:set.!Q:set (set set set) prop.(!y:set.!R:set set set set.(!z:set.z iIn y -> Q z (R z)) -> Q y (P y R)) -> Q x (P x (In_rec_iii P))