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