let X be set ; :: thesis: for L being List of X
for F being filtering Operation of X holds L | F = L WHERE F
let L be List of X; :: thesis: for F being filtering Operation of X holds L | F = L WHERE F
let F be filtering Operation of X; :: thesis: L | F = L WHERE F
thus L | F c= L WHERE F :: according to XBOOLE_0:def 10 :: thesis: L WHERE F c= L | F
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L | F or z in L WHERE F )
assume z in L | F ; :: thesis: z in L WHERE F
then consider y being Element of X such that
A1: ( z in y . F & y in L ) by Th23;
z = y by A1, Th46;
hence z in L WHERE F by A1, Th3; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in L WHERE F or z in L | F )
assume A2: z in L WHERE F ; :: thesis: z in L | F
then reconsider x = z as Element of X ;
A3: ( x in L & x . F <> {} ) by A2, Th3;
set y = the Element of x . F;
A4: [x, the Element of x . F] in F by A3, RELAT_1:169;
F c= id X by Def21;
then x = the Element of x . F by A4, RELAT_1:def 10;
hence z in L | F by A3, Th23; :: thesis: verum