let f be Function; :: thesis: ( f is involutive implies f .: (SomePoints f) c= OtherPoints f )
set F = FieldCover f;
set A1 = SomePoints f;
set A2 = OtherPoints f;
set B1 = f .: (SomePoints f);
set ch = ChoiceOn (FieldCover f);
set A = dom f;
set FP = fixpoints f;
( (f .: (SomePoints f)) \ (rng f) = {} & (OtherPoints f) \+\ (((field f) \ (fixpoints f)) /\ (rng (ChoiceOn (FieldCover f)))) = {} ) ;
then B4: ( f .: (SomePoints f) c= rng f & OtherPoints f = ((field f) \ (fixpoints f)) /\ (rng (ChoiceOn (FieldCover f))) ) by FOMODEL0:29;
assume B2: f is involutive ; :: thesis: f .: (SomePoints f) c= OtherPoints f
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (SomePoints f) or y in OtherPoints f )
assume B3: y in f .: (SomePoints f) ; :: thesis: y in OtherPoints f
then consider x being object such that
B0: ( x in dom f & x in SomePoints f & y = f . x ) by FUNCT_1:def 6;
set X = {x,(f . x)};
( {x,(f . x)} in FieldCover f & not {x,(f . x)} in {{}} ) by B0;
then {x,(f . x)} in (FieldCover f) \ {{}} by XBOOLE_0:def 5;
then B1: {x,(f . x)} in dom (ChoiceOn (FieldCover f)) by Lm9;
then ( (ChoiceOn (FieldCover f)) . {x,(f . x)} in rng (ChoiceOn (FieldCover f)) & not x in rng (ChoiceOn (FieldCover f)) ) by B0, XBOOLE_0:def 5, FUNCT_1:def 3;
then ( (ChoiceOn (FieldCover f)) . {x,(f . x)} <> x & (ChoiceOn (FieldCover f)) . {x,(f . x)} in {x,(f . x)} ) by B1, Lm9;
then ( (ChoiceOn (FieldCover f)) . {x,(f . x)} = y & x <> f . x & f . y = x ) by B0, B2, TARSKI:def 2, PARTIT_2:def 2;
then ( y in rng (ChoiceOn (FieldCover f)) & not y is_a_fixpoint_of f ) by B1, FUNCT_1:def 3, ABIAN:def 3;
then ( y in rng (ChoiceOn (FieldCover f)) & y in (rng f) null (dom f) & not y in fixpoints f ) by FOMODEL0:69, B3, B4;
then ( y in (field f) \ (fixpoints f) & y in rng (ChoiceOn (FieldCover f)) ) by XBOOLE_0:def 5;
hence y in OtherPoints f by B4, XBOOLE_0:def 4; :: thesis: verum