set X = { g where g is Element of F : g . x <> f } ;
{ g where g is Element of F : g . x <> f } c= F

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { g where g is Element of F : g . x <> f } or a in F )
assume a in { g where g is Element of F : g . x <> f } ; :: thesis: a in F
then ex g being Element of F st
( g = a & g . x <> f ) ;
hence a in F ; :: thesis: verum

end;

hence { g where g is Element of F : g . x <> f } is Subset of F ; :: thesis: verum