theorem Th39: :: HILB10_7:39

for m being Nat st m <> 0 holds
bool ((Seg (m + 2)) \ {1}) = (Ext ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m))) \/ (swap ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m)))