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