Next Prev Up
EmptyImpCS

⊢ empty ⊃ f∗ EmptyImpCS

Proof:

1
⊢ f∗≡empty ∨ f+
def. of ∗
2
⊢ empty ⊃ f∗
1,Prop

qed

Here is an straightforward corollary:

⊢ ¬f∗⊃more NotCSImpMore

Next Prev Up

2024-08-03
Contact | Home | ITL home | Course | Proofs | Algebra | FL
© 1996-2024