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: f . x = x by A2, Def3;
A4: x in dom f by A2, Def3;
dom f = E by FUNCT_2:52;
then x in union sE by A4, Th4;
then consider X being set such that
A5: x in X and
A6: X in sE by TARSKI:def 4;
f . x in f .: X by A4, A5, FUNCT_1:def 6;
then X meets f .: X by A3, A5, XBOOLE_0:3;
hence contradiction by A1, A6; :: thesis: verum