let n, m, k be Element of NAT ; :: thesis: ( PFCrt (n,m) c= PFArt (k,m) iff n < k )
thus ( PFCrt (n,m) c= PFArt (k,m) implies n < k ) :: thesis: ( n < k implies PFCrt (n,m) c= PFArt (k,m) )
proof
assume A1: PFCrt (n,m) c= PFArt (k,m) ; :: thesis: n < k
assume A2: k <= n ; :: thesis: contradiction
A3: not [((2 * n) + 1),m] in PFArt (k,m)
proof
assume A4: [((2 * n) + 1),m] in PFArt (k,m) ; :: thesis: contradiction
per cases ( ex m9 being odd Element of NAT st
( m9 <= 2 * k & [m9,m] = [((2 * n) + 1),m] ) or [(2 * k),m] = [((2 * n) + 1),m] ) by A4, Def2;
suppose A5: ex m9 being odd Element of NAT st
( m9 <= 2 * k & [m9,m] = [((2 * n) + 1),m] ) ; :: thesis: contradiction
A6: 2 * k <= 2 * n by A2, NAT_1:4;
(2 * n) + 1 <= 2 * k by A5, XTUPLE_0:1;
hence contradiction by A6, NAT_1:13; :: thesis: verum
end;
suppose [(2 * k),m] = [((2 * n) + 1),m] ; :: thesis: contradiction
hence contradiction by XTUPLE_0:1; :: thesis: verum
end;
end;
end;
[((2 * n) + 1),m] in PFCrt (n,m) by Def3;
hence contradiction by A1, A3; :: thesis: verum
end;
thus ( n < k implies PFCrt (n,m) c= PFArt (k,m) ) by Lm7; :: thesis: verum