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 Lm2;
then rng (Complement (A followed_by B)) = {(A ` ),(B ` )} by FUNCT_7:128;
then Union (Complement (A followed_by B)) = (A ` ) \/ (B ` ) by ZFMISC_1:93;
then (Union (Complement (A followed_by B))) ` = ((A ` ) ` ) /\ ((B ` ) ` ) by XBOOLE_1:53;
hence Intersection (A followed_by B) = A /\ B ; :: thesis: verum