let a be Element of r; :: thesis: a is Element of [:A,B:]
thus a is Element of [:A,B:] ; :: thesis: verum