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

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

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

proof

hence
{ g where g is Element of F : g . x <> f } is Subset of F
; :: thesis: verum
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;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