let n, m, k be Element of NAT ; :: thesis: ( n < k implies PFCrt n,m c= PFArt k,m )
assume n < k ; :: thesis: PFCrt n,m c= PFArt k,m
then 2 * n < 2 * k by XREAL_1:70;
then A1: (2 * n) + 1 <= 2 * k by NAT_1:13;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in PFCrt n,m or x in PFArt k,m )
assume x in PFCrt n,m ; :: thesis: x in PFArt k,m
then consider p being odd Element of NAT such that
A2: ( p <= (2 * n) + 1 & [p,m] = x ) by Def3;
p <= 2 * k by A1, A2, XXREAL_0:2;
hence x in PFArt k,m by A2, Def2; :: thesis: verum