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