let A be set ; :: thesis: for u being Element of (NormForm A) holds u = FinJoin ((@ u),(Atom A))
let u be Element of (NormForm A); :: thesis: u = FinJoin ((@ u),(Atom A))
thus u = FinUnion ((@ u),(singleton (DISJOINT_PAIRS A))) by SETWISEO:58
.= FinJoin ((@ u),(Atom A)) by Th9 ; :: thesis: verum