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

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

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 WHERE F or z in L | F )
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;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

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