let a, b, c, d be Element of Example; :: thesis: ( a @ a = a & a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )

thus a @ a = {} by TARSKI:def 1

.= a by TARSKI:def 1 ; :: thesis: ( a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )

thus a @ b = {} by TARSKI:def 1

.= b @ a by TARSKI:def 1 ; :: thesis: ( (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )

thus (a @ b) @ (c @ d) = {} by TARSKI:def 1

.= (a @ c) @ (b @ d) by TARSKI:def 1 ; :: thesis: ex x being Element of Example st x @ a = b

take x = a; :: thesis: x @ a = b

thus x @ a = {} by TARSKI:def 1

.= b by TARSKI:def 1 ; :: thesis: verum

thus a @ a = {} by TARSKI:def 1

.= a by TARSKI:def 1 ; :: thesis: ( a @ b = b @ a & (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )

thus a @ b = {} by TARSKI:def 1

.= b @ a by TARSKI:def 1 ; :: thesis: ( (a @ b) @ (c @ d) = (a @ c) @ (b @ d) & ex x being Element of Example st x @ a = b )

thus (a @ b) @ (c @ d) = {} by TARSKI:def 1

.= (a @ c) @ (b @ d) by TARSKI:def 1 ; :: thesis: ex x being Element of Example st x @ a = b

take x = a; :: thesis: x @ a = b

thus x @ a = {} by TARSKI:def 1

.= b by TARSKI:def 1 ; :: thesis: verum