let a, b be Element of Trivial-addLoopStr ; :: thesis: ex x being Element of Trivial-addLoopStr st x + a = b
take x = 0. Trivial-addLoopStr ; :: thesis: x + a = b
thus x + a = b by Th5; :: thesis: verum