let X be set ; for O being Operation of X holds
( O is filtering iff O = id (dom O) )
let O be Operation of X; ( O is filtering iff O = id (dom O) )
thus
( O is filtering implies O = id (dom O) )
( O = id (dom O) implies O is filtering )proof
assume A1:
O c= id X
;
MMLQUERY:def 21 O = id (dom O)
let z,
s be
object ;
RELAT_1:def 2 ( ( not [z,s] in O or [z,s] in id (dom O) ) & ( not [z,s] in id (dom O) or [z,s] in O ) )
thus
(
[z,s] in O implies
[z,s] in id (dom O) )
( not [z,s] in id (dom O) or [z,s] in O )
assume
[z,s] in id (dom O)
;
[z,s] in O
then A2:
(
z in dom O &
z = s )
by RELAT_1:def 10;
then consider y being
object such that A3:
[z,y] in O
by XTUPLE_0:def 12;
thus
[z,s] in O
by A1, A2, A3, RELAT_1:def 10;
verum
end;
assume
O = id (dom O)
; O is filtering
hence
O c= id X
by SYSREL:15; MMLQUERY:def 21 verum