let A be QC-alphabet ; :: thesis: for S1, S2 being Element of QC-Sub-WFF A st S1 `2 = S2 `2 holds
Sub_the_right_argument_of (Sub_& (S1,S2)) = S2
let S1, S2 be Element of QC-Sub-WFF A; :: thesis: ( S1 `2 = S2 `2 implies Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 )
assume A1: S1 `2 = S2 `2 ; :: thesis: Sub_the_right_argument_of (Sub_& (S1,S2)) = S2
then Sub_& (S1,S2) is Sub_conjunctive ;
hence Sub_the_right_argument_of (Sub_& (S1,S2)) = S2 by A1, Def32; :: thesis: verum