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 is without_fixpoints
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 is without_fixpoints
let sE be non empty covering Subset-Family of E; :: thesis: ( ( for X being Element of sE holds X misses f .: X ) implies f is without_fixpoints )
assume A1: for X being Element of sE holds X misses f .: X ; :: thesis: f is without_fixpoints
given x being object such that A2: x is_a_fixpoint_of f ; :: according to ABIAN:def 5 :: thesis: contradiction
A3: f . x = x by A2;
A4: x in dom f by A2;
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