set G = Complement F;
let x be object ; :: according to TARSKI:def 3,RELAT_1:def 19 :: thesis: ( not x in rng (Complement F) or x in S )
assume x in rng (Complement F) ; :: thesis: x in S
then consider y being object such that
A1: y in dom (Complement F) and
A2: x = (Complement F) . y by FUNCT_1:def 3;
reconsider y = y as Nat by A1;
(Complement F) . y = (F . y) ` by A1, Def5;
then (Complement F) . y is Event of S by PROB_1:20;
hence x in S by A2; :: thesis: verum