let V, A be set ; :: thesis: 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; :: thesis: 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 ) ) } :: according to XBOOLE_0:def 10 :: thesis: { 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))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (PP_and (p,q)) or 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 ) ) } )
assume x in dom (PP_and (p,q)) ; :: thesis: 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 ) ) }
then consider d being TypeSCNominativeData of V,A such that
A5: x = d and
A6: ( ( 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 A1, A2;

per cases ( ( 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) & d in dom (PP_not q) & (PP_not p) . d = FALSE & (PP_not q) . d = FALSE ) ) by A6;

suppose that A7: d in dom (PP_not p) and
A8: (PP_not p) . d = TRUE ; :: thesis: 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 ) ) }

p . d = FALSE by A3, A7, A8, PARTPR_1:5;
hence 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 ) ) } by A3, A5, A7; :: thesis: verum

end;

suppose that A9: d in dom (PP_not q) and
A10: (PP_not q) . d = TRUE ; :: thesis: 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 ) ) }

q . d = FALSE by A4, A9, A10, PARTPR_1:5;
hence 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 ) ) } by A4, A5, A9; :: thesis: verum

end;

suppose that A11: ( d in dom (PP_not p) & d in dom (PP_not q) ) and
A12: ( (PP_not p) . d = FALSE & (PP_not q) . d = FALSE ) ; :: thesis: 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 ) ) }

( p . d = TRUE & q . d = TRUE ) by A3, A4, A11, A12, PARTPR_1:4;
hence 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 ) ) } by A3, A4, A5, A11; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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 ) ) } ; :: thesis: 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 ) ) ;

per cases ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & d in dom q & p . d = TRUE & q . d = TRUE ) ) by A14;

suppose that A15: d in dom p and
A16: p . d = FALSE ; :: thesis: x in dom (PP_and (p,q))

(PP_not p) . d = TRUE by A15, A16, PARTPR_1:def 2;
hence x in dom (PP_and (p,q)) by A1, A2, A3, A13, A15; :: thesis: verum

end;

suppose that A17: d in dom q and
A18: q . d = FALSE ; :: thesis: x in dom (PP_and (p,q))

(PP_not q) . d = TRUE by A17, A18, PARTPR_1:def 2;
hence x in dom (PP_and (p,q)) by A1, A2, A4, A13, A17; :: thesis: verum

end;

suppose that A19: ( d in dom p & d in dom q ) and
A20: ( p . d = TRUE & q . d = TRUE ) ; :: thesis: x in dom (PP_and (p,q))

( (PP_not p) . d = FALSE & (PP_not q) . d = FALSE ) by A19, A20, PARTPR_1:def 2;
hence x in dom (PP_and (p,q)) by A1, A2, A3, A4, A13, A19; :: thesis: verum

end;

end;