Metamath Proof Explorer

Theorem shococss

Description: Inclusion in complement of complement. Part of Proposition 1 of Kalmbach p. 65. (Contributed by NM, 10-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion shococss A S A A


Step Hyp Ref Expression
1 shss A S A
2 ococss A A A
3 1 2 syl A S A A