let D be non empty set ; :: thesis: for a, b being set
for f, r, CR being File of D st a <> b & D = {a,b} & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds
( CR is_a_record_of f,CR & r is_a_record_of f,CR )
let a, b be set ; :: thesis: for f, r, CR being File of D st a <> b & D = {a,b} & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> holds
( CR is_a_record_of f,CR & r is_a_record_of f,CR )
let f, r, CR be File of D; :: thesis: ( a <> b & D = {a,b} & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> implies ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) )
assume A1: ( a <> b & D = {a,b} & CR = <*b*> & f = <*b,a,b*> & r = <*a,b*> ) ; :: thesis: ( CR is_a_record_of f,CR & r is_a_record_of f,CR )
then reconsider b2 = b, a2 = a as Element of D by Th10;
A2: CR . 1 = b by A1, FINSEQ_1:def 8;
A3: f = CR ^ r by A1, FINSEQ_1:60;
A4: len CR = 1 by A1, FINSEQ_1:57;
A5: len f = (len CR) + (len r) by A3, FINSEQ_1:35
.= 1 + (len <*a,b*>) by A1, FINSEQ_1:57
.= 1 + 2 by FINSEQ_1:61
.= 3 ;
A6: len r = 2 by A1, FINSEQ_1:61;
f = <*b,a*> ^ <*b*> by A1, FINSEQ_1:60
.= (f | 2) ^ CR by A1, Th14 ;
then ovlpart f,CR = CR by FINSEQ_8:14;
then CR /^ (len (ovlpart f,CR)) = {} by REVROT_1:2;
then f ^ (CR /^ (len (ovlpart f,CR))) = f by FINSEQ_1:47;
then A7: ovlcon f,CR = f by FINSEQ_8:def 3;
mid f,1,(len CR) = (f /^ (1 -' 1)) | ((1 -' 1) + 1) by A4, JORDAN3:def 1
.= (f /^ (1 -' 1)) | (1 + 0 ) by NAT_2:10
.= (f /^ 0 ) | 1 by NAT_D:34
.= f | 1 by FINSEQ_5:31
.= <*b2,a2,b2*> | (Seg 1) by A1, FINSEQ_1:def 15
.= CR by A1, FINSEQ_6:6 ;
then ( 1 <= len f & f is_preposition_of ) by A5, FINSEQ_8:def 8;
then A8: ( 1 <= len f & addcr f,CR is_preposition_of ) by A7, FINSEQ_8:def 11;
( 1 <= len f & CR ^ r is_substring_of f,1 ) by A3, A5, FINSEQ_8:19;
then A9: ( 1 <= len f & CR ^ r is_substring_of addcr f,CR,1 ) by A7, FINSEQ_8:def 11;
A10: r /^ (2 -' 1) = r /^ ((1 + 1) -' 1)
.= <*a2,b2*> /^ 1 by A1, NAT_D:34
.= CR by A1, FINSEQ_6:50 ;
A11: r /^ (1 -' 1) = r /^ ((0 + 1) -' 1)
.= r /^ 0 by NAT_D:34
.= r by FINSEQ_5:31 ;
A12: len CR = 1 by A1, FINSEQ_1:57;
(r /^ (1 -' 1)) . 1 = a by A1, A11, FINSEQ_1:61;
then A13: not r /^ (1 -' 1) is_preposition_of by A1, A2, A12, FINSEQ_8:21;
for j being Element of NAT st j >= 1 & j > 0 & r /^ (j -' 1) is_preposition_of holds
j >= 2

proof

let j be Element of NAT ; :: thesis: ( j >= 1 & j > 0 & r /^ (j -' 1) is_preposition_of implies j >= 2 )
assume ( j >= 1 & j > 0 & r /^ (j -' 1) is_preposition_of ) ; :: thesis: j >= 2
then j > 1 by A13, XXREAL_0:1;
then 1 + 1 <= j by NAT_1:13;
hence j >= 2 ; :: thesis: verum

end;

then A14: instr 1,r,CR = 2 by A10, FINSEQ_8:def 10;
A15: ((len r) + 1) -' (len CR) = 2 by A4, A6, NAT_D:34;
A16: CR is_terminated_by CR by FINSEQ_8:28;
r is_terminated_by CR by A4, A6, A14, A15, FINSEQ_8:def 12;
hence ( CR is_a_record_of f,CR & r is_a_record_of f,CR ) by A8, A9, A16, Def1; :: thesis: verum