let a, b, c be Int-Location; :: thesis: ( a <> b & a <> c implies not Divide (b,c) destroys a )
assume A1: ( a <> b & a <> c ) ; :: thesis: not Divide (b,c) destroys a

now :: thesis: for e being Int-Location
for l being Element of NAT
for h being FinSeq-Location holds
( a := e <> Divide (b,c) & AddTo (a,e) <> Divide (b,c) & SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) )

let e be Int-Location; :: thesis: for l being Element of NAT
for h being FinSeq-Location holds
( a := e <> Divide (b,c) & AddTo (a,e) <> Divide (b,c) & SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) )
let l be Element of NAT ; :: thesis: for h being FinSeq-Location holds
( a := e <> Divide (b,c) & AddTo (a,e) <> Divide (b,c) & SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) )
let h be FinSeq-Location ; :: thesis: ( a := e <> Divide (b,c) & AddTo (a,e) <> Divide (b,c) & SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) )
A2: InsCode (Divide (b,c)) = 5 by SCMFSA_2:22;
hence a := e <> Divide (b,c) by SCMFSA_2:18; :: thesis: ( AddTo (a,e) <> Divide (b,c) & SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) )
thus AddTo (a,e) <> Divide (b,c) by A2, SCMFSA_2:19; :: thesis: ( SubFrom (a,e) <> Divide (b,c) & MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) )
thus SubFrom (a,e) <> Divide (b,c) by A2, SCMFSA_2:20; :: thesis: ( MultBy (a,e) <> Divide (b,c) & Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) )
thus MultBy (a,e) <> Divide (b,c) by A2, SCMFSA_2:21; :: thesis: ( Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) & a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) )
thus ( Divide (e,a) <> Divide (b,c) & Divide (a,e) <> Divide (b,c) ) by A1, SF_MASTR:5; :: thesis: ( a := (h,e) <> Divide (b,c) & a :=len h <> Divide (b,c) )
thus a := (h,e) <> Divide (b,c) by A2, SCMFSA_2:26; :: thesis: a :=len h <> Divide (b,c)
thus a :=len h <> Divide (b,c) by A2, SCMFSA_2:28; :: thesis: verum

end;

hence not Divide (b,c) destroys a ; :: thesis: verum