let x, y be Element of ; :: according to STRUCT_0:def 10 :: thesis: x = y
a = x by TARSKI:def 1;
hence x = y by TARSKI:def 1; :: thesis: verum