let E be set ; :: thesis: for f being Function of E,E
for sE being non empty covering Subset-Family of E st ( for X being Element of sE holds X misses f .: X ) holds
f has_no_fixpoint
let f be Function of E,E; :: thesis: for sE being non empty covering Subset-Family of E st ( for X being Element of sE holds X misses f .: X ) holds
f has_no_fixpoint
let sE be non empty covering Subset-Family of E; :: thesis: ( ( for X being Element of sE holds X misses f .: X ) implies f has_no_fixpoint )
assume A1: for X being Element of sE holds X misses f .: X ; :: thesis: f has_no_fixpoint
given x being set such that A2: x is_a_fixpoint_of f ; :: according to ABIAN:def 5 :: thesis: contradiction
A3: ( x in dom f & f . x = x ) by A2, Def3;
dom f = E by FUNCT_2:67;
then x in union sE by A3, Th4;
then consider X being set such that
A4: ( x in X & X in sE ) by TARSKI:def 4;
f . x in f .: X by A3, A4, FUNCT_1:def 12;
then X meets f .: X by A3, A4, XBOOLE_0:3;
hence contradiction by A1, A4; :: thesis: verum