A1:
D c= D
;

consider p being PartialPredicate of D such that

A2: dom p = D and

A3: for d being object st d in dom p holds

( ( S_{1}[d] implies p . d = TRUE ) & ( not S_{1}[d] implies p . d = FALSE ) )
from PARTPR_2:sch 1(A1);

take p ; :: thesis: ( dom p = D & ( for d being object st d in dom p holds

( ( d = {} implies p . d = TRUE ) & ( d <> {} implies p . d = FALSE ) ) ) )

thus ( dom p = D & ( for d being object st d in dom p holds

( ( d = {} implies p . d = TRUE ) & ( d <> {} implies p . d = FALSE ) ) ) ) by A2, A3; :: thesis: verum

consider p being PartialPredicate of D such that

A2: dom p = D and

A3: for d being object st d in dom p holds

( ( S

take p ; :: thesis: ( dom p = D & ( for d being object st d in dom p holds

( ( d = {} implies p . d = TRUE ) & ( d <> {} implies p . d = FALSE ) ) ) )

thus ( dom p = D & ( for d being object st d in dom p holds

( ( d = {} implies p . d = TRUE ) & ( d <> {} implies p . d = FALSE ) ) ) ) by A2, A3; :: thesis: verum