let g be Function; :: thesis: ( (rng g) \ (dom g) = {} & g is involutive & (field g) \ (fixpoints g) <> {} implies ( SomePoints g <> {} & OtherPoints g <> {} ) )
assume (rng g) \ (dom g) = {} ; :: thesis: ( not g is involutive or not (field g) \ (fixpoints g) <> {} or ( SomePoints g <> {} & OtherPoints g <> {} ) )
then B0: rng g c= dom g by FOMODEL0:29;
assume B1: ( g is involutive & (field g) \ (fixpoints g) <> {} ) ; :: thesis: ( SomePoints g <> {} & OtherPoints g <> {} )
hence SomePoints g <> {} by Lm25, B0; :: thesis: OtherPoints g <> {}
then g .: (OtherPoints g) <> {} by Lm30, B0, B1;
hence OtherPoints g <> {} ; :: thesis: verum