(* definition of fan as ordered pairs *)
(* This is the correct definition to use!! *)


let CASE_FAN_FINITE = new_definition `CASE_FAN_FINITE (V,E):bool  <=> FINITE V /\ ~(V SUBSET {})`;;


let CASE_FAN_ORIGIN = new_definition `CASE_FAN_ORIGIN (V,E) <=> ~((vec 0) IN (V:real^3 -> bool))`;;


let CASE_FAN_INDEPENDENCE = 
  new_definition `CASE_FAN_INDEPENDENCE (V,E) <=> 
  (!e.  e IN E ==> ~collinear ({vec 0} UNION e))`;;
 

let CASE_FAN_INTERSECTION =  
  new_definition`CASE_FAN_INTERSECTION(V,E):bool<=> 
  (!e1 e2. (e1 IN E UNION {{v}| v IN V}) /\ (e2 IN E UNION {{v}| v IN V})
  ==> ((aff_ge {vec 0 } e1) INTER (aff_ge {vec 0} e2) = aff_ge {vec 0} (e1 INTER e2)))`;;



let FANO=new_definition`FANO(V,E) <=> 
  ((UNIONS E) SUBSET V) /\ graph(E) /\ CASE_FAN_FINITE(V,E) /\ CASE_FAN_ORIGIN(V,E)/\
  CASE_FAN_INDEPENDENCE(V,E)/\ CASE_FAN_INTERSECTION(V,E)`;;


let FANO_OF_FAN = 
prove( `!V E. (FAN(vec 0 , V , E) <=> FANO(V,E))`,