let T be non empty RelStr ; :: thesis: for A, B being Subset of T
for n being Element of NAT holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `
let A, B be Subset of T; :: thesis: for n being Element of NAT holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `
let n be Element of NAT ; :: thesis: (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `
(Fdfl (A,n)) /\ (Fdfl (B,n)) = Fdfl ((A /\ B),n) by Th42
.= (Finf (((A /\ B) `),n)) ` by Th45 ;
hence (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) ` ; :: thesis: verum