theorem :: ARMSTRNG:13

for X being set
for A, B, A9, B9 being Subset of X holds
( [A,B] >= [A9,B9] iff ( A c= A9 & B9 c= B ) ) ;