let B be set ; :: thesis: for t, a being object holds
( a is B \/ {t} -axiomatic iff ( a is B -axiomatic or a = t ) )
let t, a be object ; :: thesis: ( a is B \/ {t} -axiomatic iff ( a is B -axiomatic or a = t ) )
set C = B \/ {t};
thus ( not a is B \/ {t} -axiomatic or a is B -axiomatic or a = t ) :: thesis: ( ( a is B -axiomatic or a = t ) implies a is B \/ {t} -axiomatic )

proof

assume a is B \/ {t} -axiomatic ; :: thesis: ( a is B -axiomatic or a = t )
then ( a in B or a in {t} ) by XBOOLE_0:def 3;
hence ( a is B -axiomatic or a = t ) by TARSKI:def 1; :: thesis: verum

end;

assume ( a is B -axiomatic or a = t ) ; :: thesis: a is B \/ {t} -axiomatic
then ( a in B or a in {t} ) by TARSKI:def 1;
hence a is B \/ {t} -axiomatic by XBOOLE_0:def 3; :: thesis: verum