a is set by TARSKI:1;
then consider i being Element of I such that
A1: i <> a by SUBSET_1:50;
take i ; :: thesis: i is a -different
thus i <> a by A1; :: according to MSAFREE5:def 3 :: thesis: verum