set R = F_Rat ;
set x = the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat));

now :: thesis: F_Rat is polynomial_disjoint

assume not F_Rat is polynomial_disjoint ; :: thesis: contradiction
then A1: ( the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) in [#] F_Rat & the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) in [#] (Polynom-Ring F_Rat) ) by XBOOLE_0:def 4;
then reconsider p = the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) as Polynomial of F_Rat by POLYNOM3:def 10;
reconsider x = the Element of ([#] F_Rat) /\ ([#] (Polynom-Ring F_Rat)) as Rational by A1;
p = x ;
hence contradiction by Th20; :: thesis: verum

end;

hence F_Rat is polynomial_disjoint ; :: thesis: verum