A1: {2,3} <> {1,2,3,4}
proof
assume {2,3} = {1,2,3,4} ; :: thesis: contradiction
then 1 in {2,3} by ENUMSET1:def 2;
hence contradiction by TARSKI:def 2; :: thesis: verum
end;
A2: {2,3} <> {1,2,3}
proof
assume {2,3} = {1,2,3} ; :: thesis: contradiction
then 1 in {2,3} by ENUMSET1:def 1;
hence contradiction by TARSKI:def 2; :: thesis: verum
end;
A3: {2,3} <> {2,3,4}
proof
assume {2,3} = {2,3,4} ; :: thesis: contradiction
then 4 in {2,3} by ENUMSET1:def 1;
hence contradiction by TARSKI:def 2; :: thesis: verum
end;
A4: {2,3} <> {1} by ZFMISC_1:5;
A5: {2,3} <> {2} by ZFMISC_1:5;
A6: {2,3} <> {3} by ZFMISC_1:5;
{2,3} <> {4} by ZFMISC_1:5;
hence not {1,2,3} /\ {2,3,4} in sring4_8 by LL10, A1, A2, A3, A4, A5, A6, ENUMSET1:def 6; :: thesis: verum