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

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