let G be non empty DTConstrStr ; :: thesis: for n, m being String of G st n ==> m holds
m is_derivable_from n
let n, m be String of G; :: thesis: ( n ==> m implies m is_derivable_from n )
assume A1: n ==> m ; :: thesis: m is_derivable_from n
take p = <*n,m*>; :: according to LANG1:def 5 :: thesis: ( len p >= 1 & p . 1 = n & p . (len p) = m & ( for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) ) )
A2: len p = 2 by FINSEQ_1:44;
hence ( len p >= 1 & p . 1 = n & p . (len p) = m ) ; :: thesis: for i being Element of NAT st i >= 1 & i < len p holds
ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
let i be Element of NAT ; :: thesis: ( i >= 1 & i < len p implies ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b ) )
assume that
A3: i >= 1 and
A4: i < len p ; :: thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
take a = n; :: thesis: ex b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
take b = m; :: thesis: ( p . i = a & p . (i + 1) = b & a ==> b )
2 = 1 + 1 ;
then i <= 1 by A2, A4, NAT_1:13;
then A5: i = 1 by A3, XXREAL_0:1;
hence p . i = a ; :: thesis: ( p . (i + 1) = b & a ==> b )
thus p . (i + 1) = b by A5; :: thesis: a ==> b
thus a ==> b by A1; :: thesis: verum