let X, z be set ; :: thesis: for x being Element of X

for F being filtering Operation of X st z in x . F holds

z = x

let x be Element of X; :: thesis: for F being filtering Operation of X st z in x . F holds

z = x

let F be filtering Operation of X; :: thesis: ( z in x . F implies z = x )

assume z in x . F ; :: thesis: z = x

then ( [x,z] in F & F c= id X ) by Def21, RELAT_1:169;

hence z = x by RELAT_1:def 10; :: thesis: verum

for F being filtering Operation of X st z in x . F holds

z = x

let x be Element of X; :: thesis: for F being filtering Operation of X st z in x . F holds

z = x

let F be filtering Operation of X; :: thesis: ( z in x . F implies z = x )

assume z in x . F ; :: thesis: z = x

then ( [x,z] in F & F c= id X ) by Def21, RELAT_1:169;

hence z = x by RELAT_1:def 10; :: thesis: verum