let E be Event of ; :: thesis: E is Subset of X
E in F ;
hence E is Subset of X ; :: thesis: verum