let T be non empty RelStr ; for A, B being Subset of T
for n being Nat holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
let A, B be Subset of T; for n being Nat holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
let n be Nat; Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
for n being Nat holds (Fcl (A \/ B)) . n = ((Fcl A) . n) \/ ((Fcl B) . n)
hence
Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
; verum