begin
theorem Th1:
:: deftheorem Def1 defines '/\' BVFUNC_2:def 1 :
:: deftheorem Def2 defines is_upper_min_depend_of BVFUNC_2:def 2 :
theorem Th2:
:: deftheorem Def3 defines '\/' BVFUNC_2:def 3 :
theorem
theorem
begin
:: deftheorem defines generating BVFUNC_2:def 4 :
:: deftheorem defines independent BVFUNC_2:def 5 :
:: deftheorem defines is_a_coordinate BVFUNC_2:def 6 :
:: deftheorem defines CompF BVFUNC_2:def 7 :
:: deftheorem Def8 defines is_independent_of BVFUNC_2:def 8 :
:: deftheorem defines All BVFUNC_2:def 9 :
:: deftheorem defines Ex BVFUNC_2:def 10 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th24:
theorem
theorem
theorem Th27:
theorem
theorem
theorem Th30:
theorem
theorem Th32:
theorem
theorem Th34:
theorem
theorem Th36:
theorem
theorem
theorem
theorem Th40:
theorem