A1:
{2,3} <> {1,2,3,4}
A2:
{2,3} <> {1,2,3}
A3:
{2,3} <> {2,3,4}
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; verum