set z = [(1_. L),(1_. L)];
set p1 = [(1_. L),(1_. L)] `1 ;
set p2 = [(1_. L),(1_. L)] `2 ;
now :: thesis: not [(1_. L),(1_. L)] `1 ,[(1_. L),(1_. L)] `2 have_a_common_root
assume [(1_. L),(1_. L)] `1 ,[(1_. L),(1_. L)] `2 have_a_common_root ; :: thesis: contradiction
then consider x being Element of L such that
A1: x is_a_common_root_of [(1_. L),(1_. L)] `1 ,[(1_. L),(1_. L)] `2 ;
x is_a_root_of [(1_. L),(1_. L)] `2 by A1;
then eval (([(1_. L),(1_. L)] `2),x) = 0. L by POLYNOM5:def 7;
hence contradiction by POLYNOM4:18; :: thesis: verum
end;
hence 1._ L is irreducible ; :: thesis: verum