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 A1: ( x in the carrier of H & y in the carrier of H ) ; :: thesis: x \ y in the carrier of H
reconsider x1 = x, y1 = y as Element of H by A1;
x \ y = x1 \ y1 by Th38;
hence x \ y in the carrier of H ; :: thesis: verum