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

x in Borel_Sets ;

hence [(p `1),((p `2) `)] is Element of Prop Q by ZFMISC_1:87; :: thesis: verum