let n be Nat; :: thesis: for f being FinSequence of (TOP-REAL n) holds
( ( len f = 0 or len f = 1 ) iff L~ f = {} )
let f be FinSequence of (TOP-REAL n); :: thesis: ( ( len f = 0 or len f = 1 ) iff L~ f = {} )
thus ( ( len f = 0 or len f = 1 ) implies L~ f = {} ) :: thesis: ( not L~ f = {} or len f = 0 or len f = 1 )
proof
set L = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
set x = the Element of { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
assume A1: ( len f = 0 or len f = 1 ) ; :: thesis: L~ f = {}
now :: thesis: L~ f = {}
per cases ( len f = 0 or len f = 0 + 1 ) by A1;
suppose A2: len f = 0 ; :: thesis: L~ f = {}
now :: thesis: not { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } <> {}
assume { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } <> {} ; :: thesis: contradiction
then the Element of { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
then ex i being Nat st
( the Element of { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } = LSeg (f,i) & 1 <= i & i + 1 <= len f ) ;
hence contradiction by A2; :: thesis: verum
end;
hence L~ f = {} by ZFMISC_1:2; :: thesis: verum
end;
suppose A3: len f = 0 + 1 ; :: thesis: L~ f = {}
now :: thesis: not { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } <> {}
assume { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } <> {} ; :: thesis: contradiction
then the Element of { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
then ex i being Nat st
( the Element of { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } = LSeg (f,i) & 1 <= i & i + 1 <= len f ) ;
hence contradiction by A3, XREAL_1:6; :: thesis: verum
end;
hence L~ f = {} by ZFMISC_1:2; :: thesis: verum
end;
end;
end;
hence L~ f = {} ; :: thesis: verum
end;
set L = { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
assume A4: L~ f = {} ; :: thesis: ( len f = 0 or len f = 1 )
assume that
A5: len f <> 0 and
A6: len f <> 1 ; :: thesis: contradiction
now :: thesis: not len f <= 1
assume len f <= 1 ; :: thesis: contradiction
then len f < 0 + 1 by A6, XXREAL_0:1;
hence contradiction by A5, NAT_1:13; :: thesis: verum
end;
then A7: len f >= 1 + 1 by NAT_1:13;
then LSeg (f,1) in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } ;
then LSeg (f,1) = {} by A4, XBOOLE_1:3, ZFMISC_1:74;
hence contradiction by A7, Th21; :: thesis: verum