let Q be multLoop; :: thesis: for H being SubLoop of Q
for x, y being Element of Q st x in the carrier of H & y in the carrier of H holds
x / y in the carrier of H
let H be SubLoop of Q; :: thesis: for x, y being Element of Q st x in the carrier of H & y in the carrier of H holds
x / y in the carrier of H
let x, y be Element of Q; :: thesis: ( x in the carrier of H & y in the carrier of H implies x / y in the carrier of H )
assume ( x in the carrier of H & y in the carrier of H ) ; :: thesis: x / y in the carrier of H
then reconsider x1 = x, y1 = y as Element of H ;
x / y = x1 / y1 by Th40;
hence x / y in the carrier of H ; :: thesis: verum