assume [P,Q,R1,R2] : (line(P) & line(Q) & int_l_l(P,Q) & plane(R1) & plane(R2) & inc_l_pl(P,R1) & inc_l_pl(P,R2) & inc_l_pl(Q,R1) & inc_l_pl(Q,R2))
infer (R1=R2)
