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