let x be object ; :: thesis: for D being non empty set
for p, q being PartialPredicate of D holds
( not x in dom (PP_or (p,q)) or ( x in dom p & p . x = TRUE ) or ( x in dom q & q . x = TRUE ) or ( x in dom p & p . x = FALSE & x in dom q & q . x = FALSE ) )
let D be non empty set ; :: thesis: for p, q being PartialPredicate of D holds
( not x in dom (PP_or (p,q)) or ( x in dom p & p . x = TRUE ) or ( x in dom q & q . x = TRUE ) or ( x in dom p & p . x = FALSE & x in dom q & q . x = FALSE ) )
let p, q be PartialPredicate of D; :: thesis: ( not x in dom (PP_or (p,q)) or ( x in dom p & p . x = TRUE ) or ( x in dom q & q . x = TRUE ) or ( x in dom p & p . x = FALSE & x in dom q & q . x = FALSE ) )
assume A1: x in dom (PP_or (p,q)) ; :: thesis: ( ( x in dom p & p . x = TRUE ) or ( x in dom q & q . x = TRUE ) or ( x in dom p & p . x = FALSE & x in dom q & q . x = FALSE ) )
dom (PP_or (p,q)) = { d where d is Element of D : ( ( 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 ) ) } by Def4;
then ex d1 being Element of D st
( d1 = x & ( ( d1 in dom p & p . d1 = TRUE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = FALSE & d1 in dom q & q . d1 = FALSE ) ) ) by A1;
hence ( ( x in dom p & p . x = TRUE ) or ( x in dom q & q . x = TRUE ) or ( x in dom p & p . x = FALSE & x in dom q & q . x = FALSE ) ) ; :: thesis: verum