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