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