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