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