let a be ordinal number ; :: thesis: for A being empty set holds A is a -based
let A be empty set ; :: thesis: A is a -based
let b be ordinal number ; :: according to EXCHSORT:def 2 :: thesis: ( b in proj1 A implies ( a in proj1 A & a c= b ) )
thus ( b in proj1 A implies ( a in proj1 A & a c= b ) ) ; :: thesis: verum