let i be set ; :: according to PBOOLE:def 15 :: 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 set such that
A2: x in (MSFixPoints F) . i by XBOOLE_0:def 1;
consider f being Function such that
A3: ( f = F . i & x in dom f & f . x = x ) by A1, A2, Def13;
M . i = {} by A1, PBOOLE:def 15;
then f is Function of {} ,{} by A1, A3, PBOOLE:def 18;
hence contradiction by A3; :: thesis: verum