let x be object ; :: thesis: for D being set
for p being PartialPredicate of D holds
( p . x = TRUE or p . x = FALSE )
let D be set ; :: thesis: for p being PartialPredicate of D holds
( p . x = TRUE or p . x = FALSE )
let p be PartialPredicate of D; :: thesis: ( p . x = TRUE or p . x = FALSE )
assume A1: p . x <> TRUE ; :: thesis: p . x = FALSE
A2: rng p c= BOOLEAN by RELAT_1:def 19;

per cases ( x in dom p or not x in dom p ) ;

suppose x in dom p ; :: thesis: p . x = FALSE

then p . x in rng p by FUNCT_1:3;
hence p . x = FALSE by A1, A2, TARSKI:def 2; :: thesis: verum

end;

suppose not x in dom p ; :: thesis: p . x = FALSE

hence p . x = FALSE by FUNCT_1:def 2; :: thesis: verum

end;

end;