let T be non empty RelStr ; for A, B being Subset of T
for n being Nat holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `
let A, B be Subset of T; for n being Nat holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `
let n be Nat; (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)) `
; verum