let i be object ; :: according to PBOOLE:def 12 :: thesis: ( not i in I or (MSFixPoints F) . i is empty )
assume A1: i in I ; :: thesis: (MSFixPoints F) . i is empty
assume not (MSFixPoints F) . i is empty ; :: thesis: contradiction
then consider x being object such that
A2: x in (MSFixPoints F) . i ;
consider f being Function such that
A3: f = F . i and
A4: x in dom f and
f . x = x by A1, A2, Def12;
M . i = {} ;
then f is Function of {},{} by A1, A3, PBOOLE:def 15;
hence contradiction by A4; :: thesis: verum