theorem :: ARMSTRNG:24

for X being set
for K being Subset of X holds { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } is Full-family of X