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
B: x is_a_common_root_of [(1_. L),(1_. L)] `1 ,[(1_. L),(1_. L)] `2 by root2;
x is_a_root_of [(1_. L),(1_. L)] `2 by B, root1;
then eval (([(1_. L),(1_. L)] `2),x) = 0. L by POLYNOM5:def 6;
hence contradiction by POLYNOM4:18; :: thesis: verum

end;

hence 1._ L is irreducible by defirred; :: thesis: verum