let V, A be set ; for p, q being SCPartialNominativePredicate of V,A holds dom (PP_and (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) }
let p, q be SCPartialNominativePredicate of V,A; dom (PP_and (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) }
set F = PP_and (p,q);
set P = PP_not p;
set Q = PP_not q;
set D = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) } ;
A1:
dom (PP_and (p,q)) = dom (PP_or ((PP_not p),(PP_not q)))
by PARTPR_1:def 2;
A2:
dom (PP_or ((PP_not p),(PP_not q))) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom (PP_not p) & (PP_not p) . d = TRUE ) or ( d in dom (PP_not q) & (PP_not q) . d = TRUE ) or ( d in dom (PP_not p) & (PP_not p) . d = FALSE & d in dom (PP_not q) & (PP_not q) . d = FALSE ) ) }
by Th15;
A3:
dom (PP_not p) = dom p
by PARTPR_1:def 2;
A4:
dom (PP_not q) = dom q
by PARTPR_1:def 2;
thus
dom (PP_and (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 = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) }
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 = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) } c= dom (PP_and (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 = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) } or x in dom (PP_and (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 = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) }
; x in dom (PP_and (p,q))
then consider d being TypeSCNominativeData of V,A such that
A13:
x = d
and
A14:
( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) )
;