let V, A be set ; for p, q being SCPartialNominativePredicate of V,A holds dom (PP_imp (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }
let p, q be SCPartialNominativePredicate of V,A; dom (PP_imp (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }
set F = PP_imp (p,q);
set P = PP_not p;
set D = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) } ;
A1:
dom (PP_imp (p,q)) = { d where d is Element of ND (V,A) : ( ( d in dom (PP_not p) & (PP_not p) . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom (PP_not p) & (PP_not p) . d = FALSE & d in dom q & q . d = FALSE ) ) }
by PARTPR_1:def 4;
A2:
dom (PP_not p) = dom p
by PARTPR_1:def 2;
thus
dom (PP_imp (p,q)) c= { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }
XBOOLE_0:def 10 { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) } c= dom (PP_imp (p,q))
let x be object ; TARSKI:def 3 ( not x in { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) } or x in dom (PP_imp (p,q)) )
assume
x in { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }
; x in dom (PP_imp (p,q))
then consider d being TypeSCNominativeData of V,A such that
A10:
x = d
and
A11:
( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) )
;