[isabelle] [Isabelle] how to translate this into Isabelle language to prove the this



Hi sir,
Every poset is in which every chain has  an upper bound has a maximal element  =>  prove every  vector  space has a basis.
Every poset is in which every chain has  an upper bound has a maximal element  =>  prove  every connected graph  has a spanning tree.

Regards,
Martin Lee 		 	   		  


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.