let B be antichain; :: thesis: B is B -headed
B = B ^ {{}} by Th3;
hence B is B -headed ; :: thesis: verum