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 & p . 1 = n & p . 2 = m ) by FINSEQ_1:61;
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 A3: ( i >= 1 & i < len p ) ; :: thesis: ex a, b being String of G st
( p . i = a & p . (i + 1) = b & a ==> b )
2 = 1 + 1 ;
then i <= 1 by A2, A3, NAT_1:13;
then A4: i = 1 by A3, XXREAL_0:1;
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 )
thus p . i = a by A4, FINSEQ_1:61; :: thesis: ( p . (i + 1) = b & a ==> b )
thus p . (i + 1) = b by A4, FINSEQ_1:61; :: thesis: a ==> b
thus a ==> b by A1; :: thesis: verum