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:68;
then A1: (2 * n) + 1 <= 2 * k by NAT_1:13;
let x be object ; :: 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 and
A3: [p,m] = x by Def3;
p <= 2 * k by A1, A2, XXREAL_0:2;
hence x in PFArt (k,m) by A3, Def2; :: thesis: verum