let x be object ; :: thesis: for D being set
for p being PartialPredicate of D holds
( not x in dom p or p . x = TRUE or p . x = FALSE )
let D be set ; :: thesis: for p being PartialPredicate of D holds
( not x in dom p or p . x = TRUE or p . x = FALSE )
let p be PartialPredicate of D; :: thesis: ( not x in dom p or p . x = TRUE or p . x = FALSE )
assume A1: x in dom p ; :: thesis: ( p . x = TRUE or p . x = FALSE )
A2: rng p c= BOOLEAN by RELAT_1:def 19;
p . x in rng p by A1, FUNCT_1:3;
hence ( p . x = TRUE or p . x = FALSE ) by A2, TARSKI:def 2; :: thesis: verum