let X be set ; :: thesis: for A, B being Subset of X holds Intersection (A followed_by B) = A /\ B

let A, B be Subset of X; :: thesis: Intersection (A followed_by B) = A /\ B

set A1 = A followed_by B;

Complement (A followed_by B) = (A `) followed_by (B `) by Lm1;

then rng (Complement (A followed_by B)) = {(A `),(B `)} by FUNCT_7:126;

then Union (Complement (A followed_by B)) = (A `) \/ (B `) by ZFMISC_1:75;

then (Union (Complement (A followed_by B))) ` = ((A `) `) /\ ((B `) `) by XBOOLE_1:53;

hence Intersection (A followed_by B) = A /\ B ; :: thesis: verum

let A, B be Subset of X; :: thesis: Intersection (A followed_by B) = A /\ B

set A1 = A followed_by B;

Complement (A followed_by B) = (A `) followed_by (B `) by Lm1;

then rng (Complement (A followed_by B)) = {(A `),(B `)} by FUNCT_7:126;

then Union (Complement (A followed_by B)) = (A `) \/ (B `) by ZFMISC_1:75;

then (Union (Complement (A followed_by B))) ` = ((A `) `) /\ ((B `) `) by XBOOLE_1:53;

hence Intersection (A followed_by B) = A /\ B ; :: thesis: verum