let X be set ; :: thesis: for O being Operation of X holds
( O is filtering iff O = id (dom O) )
let O be Operation of X; :: thesis: ( O is filtering iff O = id (dom O) )
thus ( O is filtering implies O = id (dom O) ) :: thesis: ( O = id (dom O) implies O is filtering )
proof
assume A1: O c= id X ; :: according to MMLQUERY:def 21 :: thesis: O = id (dom O)
let z, s be object ; :: according to RELAT_1:def 2 :: thesis: ( ( 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) ) :: thesis: ( not [z,s] in id (dom O) or [z,s] in O )
proof
assume [z,s] in O ; :: thesis: [z,s] in id (dom O)
then ( z in dom O & z = s ) by A1, RELAT_1:def 10, XTUPLE_0:def 12;
hence [z,s] in id (dom O) by RELAT_1:def 10; :: thesis: verum
end;
assume [z,s] in id (dom O) ; :: thesis: [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; :: thesis: verum
end;
assume O = id (dom O) ; :: thesis: O is filtering
hence O c= id X by SYSREL:15; :: according to MMLQUERY:def 21 :: thesis: verum