let MySigmaField, A1, A2 be set ; :: thesis: ( MySigmaField = {{},{1,2,3,4}} & A1 in MySigmaField & A2 in MySigmaField implies A1 /\ A2 in MySigmaField )
assume A0: ( MySigmaField = {{},{1,2,3,4}} & A1 in MySigmaField & A2 in MySigmaField ) ; :: thesis: A1 /\ A2 in MySigmaField
then ( ( A1 = {} or A1 = {1,2,3,4} ) & ( A2 = {} or A2 = {1,2,3,4} ) ) by TARSKI:def 2;
hence A1 /\ A2 in MySigmaField by A0; :: thesis: verum