let D be non empty set ; :: thesis: for p being PartialPredicate of D holds <*p,(PPid D),p*> is SFHT of D
let p be PartialPredicate of D; :: thesis: <*p,(PPid D),p*> is SFHT of D
set f = PPid D;
for d being Element of D st d in dom p & p . d = TRUE & d in dom (PPid D) & (PPid D) . d in dom p holds
p . ((PPid D) . d) = TRUE ;
then <*p,(PPid D),p*> in SFHTs D ;
hence <*p,(PPid D),p*> is SFHT of D ; :: thesis: verum