Metamath Proof Explorer

Table of Contents - 21.3.28.3. Outer Five Segment (not used, no need to move to main)

1. cafs
2. df-afs
3. afsval
4. brafs
5. tg5segofs