reconsider x = (p `2) ` as Event of Borel_Sets by PROB_1:20;
x in Borel_Sets ;
hence [(p `1),((p `2) `)] is Element of Prop Q by ZFMISC_1:87; :: thesis: verum