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₁[d] implies p . d = TRUE ) & ( not S₁[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