let g be Function; :: thesis: ( g is involutive & (field g) \ (fixpoints g) <> {} & rng g c= dom g implies SomePoints g <> {} )
assume g is involutive ; :: thesis: ( not (field g) \ (fixpoints g) <> {} or not rng g c= dom g or SomePoints g <> {} )
then reconsider gg = g as involutive Function ;
set G = field gg;
set F = fixpoints gg;
set S = SomePoints gg;
set O = OtherPoints gg;
assume B0: (field g) \ (fixpoints g) <> {} ; :: thesis: ( not rng g c= dom g or SomePoints g <> {} )
then reconsider G = field gg as non empty set ;
reconsider X = G \ (fixpoints gg) as non empty Subset of G by B0;
assume B2: rng g c= dom g ; :: thesis: SomePoints g <> {}
assume SomePoints g = {} ; :: thesis: contradiction
then reconsider S = SomePoints gg as empty Subset of G ;
X \ S <> {} ;
then reconsider O = OtherPoints gg as non empty Subset of G ;
gg .: S = O by B2, Lm30;
hence contradiction ; :: thesis: verum