let p be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st X |- p holds

X |- 'X' p

let X be Subset of LTLB_WFF; :: thesis: ( X |- p implies X |- 'X' p )

assume X |- p ; :: thesis: X |- 'X' p

then consider f being FinSequence of LTLB_WFF such that

A1: f . (len f) = p and

A2: 1 <= len f and

A3: for i being Nat st 1 <= i & i <= len f holds

prc f,X,i ;

set g = f ^ <*('X' p)*>;

A4: len (f ^ <*('X' p)*>) = (len f) + (len <*('X' p)*>) by FINSEQ_1:22

.= (len f) + 1 by FINSEQ_1:39 ;

then A5: len f < len (f ^ <*('X' p)*>) by NAT_1:16;

then A6: (f ^ <*('X' p)*>) /. (len f) = (f ^ <*('X' p)*>) . (len f) by A2, Lm1

.= p by A1, A2, FINSEQ_1:64 ;

1 <= len (f ^ <*('X' p)*>) by A2, A4, NAT_1:16;

then (f ^ <*('X' p)*>) /. (len (f ^ <*('X' p)*>)) = (f ^ <*('X' p)*>) . (len (f ^ <*('X' p)*>)) by Lm1

.= 'X' ((f ^ <*('X' p)*>) /. (len f)) by A4, A6, FINSEQ_1:42 ;

then (f ^ <*('X' p)*>) /. (len f) NEX_rule (f ^ <*('X' p)*>) /. (len (f ^ <*('X' p)*>)) ;

then prc f ^ <*('X' p)*>,X, len (f ^ <*('X' p)*>) by A2, A5;

hence X |- 'X' p by A2, A3, Th40; :: thesis: verum

X |- 'X' p

let X be Subset of LTLB_WFF; :: thesis: ( X |- p implies X |- 'X' p )

assume X |- p ; :: thesis: X |- 'X' p

then consider f being FinSequence of LTLB_WFF such that

A1: f . (len f) = p and

A2: 1 <= len f and

A3: for i being Nat st 1 <= i & i <= len f holds

prc f,X,i ;

set g = f ^ <*('X' p)*>;

A4: len (f ^ <*('X' p)*>) = (len f) + (len <*('X' p)*>) by FINSEQ_1:22

.= (len f) + 1 by FINSEQ_1:39 ;

then A5: len f < len (f ^ <*('X' p)*>) by NAT_1:16;

then A6: (f ^ <*('X' p)*>) /. (len f) = (f ^ <*('X' p)*>) . (len f) by A2, Lm1

.= p by A1, A2, FINSEQ_1:64 ;

1 <= len (f ^ <*('X' p)*>) by A2, A4, NAT_1:16;

then (f ^ <*('X' p)*>) /. (len (f ^ <*('X' p)*>)) = (f ^ <*('X' p)*>) . (len (f ^ <*('X' p)*>)) by Lm1

.= 'X' ((f ^ <*('X' p)*>) /. (len f)) by A4, A6, FINSEQ_1:42 ;

then (f ^ <*('X' p)*>) /. (len f) NEX_rule (f ^ <*('X' p)*>) /. (len (f ^ <*('X' p)*>)) ;

then prc f ^ <*('X' p)*>,X, len (f ^ <*('X' p)*>) by A2, A5;

hence X |- 'X' p by A2, A3, Th40; :: thesis: verum