let L be non empty right_complementable add-associative right_zeroed addLoopStr ; for z0, z1, z2, z3 being Element of L holds <%z0,z1%> - <%z2,z3%> = <%(z0 - z2),(z1 - z3)%>
let z0, z1, z2, z3 be Element of L; <%z0,z1%> - <%z2,z3%> = <%(z0 - z2),(z1 - z3)%>
thus <%z0,z1%> - <%z2,z3%> =
<%z0,z1%> + <%(- z2),(- z3)%>
by Th31
.=
<%(z0 - z2),(z1 - z3)%>
by Th28
; verum