let a, b be Element of Trivial-addLoopStr ; :: thesis: a = b
thus a = {} by CARD_1:87, TARSKI:def 1
.= b by CARD_1:87, TARSKI:def 1 ; :: thesis: verum