theorem Th15: :: NOMIN_2:16

for V, A being set
for p, q being SCPartialNominativePredicate of V,A holds dom (PP_or (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) }