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 CARD_1:49, TARSKI:def 1
.= a by CARD_1:49, 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 CARD_1:49, TARSKI:def 1
.= b @ a by CARD_1:49, 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 CARD_1:49, TARSKI:def 1
.= (a @ c) @ (b @ d) by CARD_1:49, 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 CARD_1:49, TARSKI:def 1
.= b by CARD_1:49, TARSKI:def 1 ; :: thesis: verum