let T be non empty RelStr ; :: thesis: for A, B being Subset of T
for n being Element of NAT holds (Fint A,n) /\ (Fint B,n) = (Fcl ((A /\ B) ` ),n) `
let A, B be Subset of T; :: thesis: for n being Element of NAT holds (Fint A,n) /\ (Fint B,n) = (Fcl ((A /\ B) ` ),n) `
let n be Element of NAT ; :: thesis: (Fint A,n) /\ (Fint B,n) = (Fcl ((A /\ B) ` ),n) `
(Fint A,n) /\ (Fint B,n) = Fint (A /\ B),n by Th22
.= (Fcl ((A /\ B) ` ),n) ` by Th28 ;
hence (Fint A,n) /\ (Fint B,n) = (Fcl ((A /\ B) ` ),n) ` ; :: thesis: verum