let n be Nat; :: thesis: divisors ((5 |^ n),4,3) = {}
set A = divisors ((5 |^ n),4,3);
{} = divisors ((5 |^ n),4,3)

proof

thus {} c= divisors ((5 |^ n),4,3) ; :: according to XBOOLE_0:def 10 :: thesis: divisors ((5 |^ n),4,3) c= {}
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in divisors ((5 |^ n),4,3) or x in {} )
assume x in divisors ((5 |^ n),4,3) ; :: thesis: x in {}
then ex k being Nat st
( x = k & k mod 4 = 3 & k divides 5 |^ n ) ;
hence x in {} by Th34; :: thesis: verum

end;

hence divisors ((5 |^ n),4,3) = {} ; :: thesis: verum