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

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