let m be Nat; :: thesis: ( m <> 0 implies 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))) )
assume A1: m <> 0 ; :: thesis: 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)))
set s = (Seg (m + 1)) \ {1};
set F = bool ((Seg (m + 1)) \ {1});
set F1 = bool ((Seg (m + 2)) \ {1});
set E = Ext ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m));
set S = swap ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m));
(1 + m) + 1 > m + 1 by NAT_1:13;
then not m + 2 in Seg (m + 1) by FINSEQ_1:1;
then A2: not 2 + m in union (bool ((Seg (m + 1)) \ {1})) by ZFMISC_1:56;
then A3: ( card (swap ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m))) = card (bool ((Seg (m + 1)) \ {1})) & card (bool ((Seg (m + 1)) \ {1})) = card (Ext ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m))) ) by Th10, Th11;
A4: 2 * (card (bool ((Seg (m + 1)) \ {1}))) = card (bool ((Seg (1 + (m + 1))) \ {1})) by Th9
.= card (bool ((Seg (m + 2)) \ {1})) ;
1 + m <> 2 + m ;
then A5: card ((Ext ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m))) \/ (swap ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m)))) = (card (bool ((Seg (m + 1)) \ {1}))) + (card (bool ((Seg (m + 1)) \ {1}))) by Th22, A2, A3, CARD_2:40
.= card (bool ((Seg (m + 2)) \ {1})) by A4 ;
A6: ( Seg ((m + 1) + 1) = (Seg (m + 1)) \/ {(m + 2)} & Seg (m + 1) = (Seg m) \/ {(m + 1)} ) by FINSEQ_1:9;
then ( (Seg ((m + 1) + 1)) \ {1} = ((Seg (m + 1)) \ {1}) \/ ({(m + 2)} \ {1}) & 1 <> m + 2 ) by A1, XBOOLE_1:42;
then A7: (Seg ((m + 1) + 1)) \ {1} = ((Seg (m + 1)) \ {1}) \/ {(m + 2)} by ZFMISC_1:14;
m + 1 <> 1 by A1;
then ( {(m + 1)} c= Seg (m + 1) & not 1 in {(m + 1)} ) by A6, XBOOLE_1:7, TARSKI:def 1;
then A8: ( (Seg ((m + 1) + 1)) \ {1} = (((Seg (m + 1)) \ {1}) \/ {(m + 1)}) \/ {(m + 2)} & (((Seg (m + 1)) \ {1}) \/ {(m + 1)}) \/ {(m + 2)} = ((Seg (m + 1)) \ {1}) \/ {(m + 2)} ) by A7, XBOOLE_1:12, ZFMISC_1:34;
A9: swap ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m)) c= bool ((Seg (m + 2)) \ {1})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in swap ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m)) or x in bool ((Seg (m + 2)) \ {1}) )
assume A10: x in swap ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m)) ; :: thesis: x in bool ((Seg (m + 2)) \ {1})
reconsider x = x as set by TARSKI:1;

per cases ( x in { ((A \ {(m + 1)}) \/ {(m + 2)}) where A is Element of bool ((Seg (m + 1)) \ {1}) : m + 1 in A } or x in { (A \/ {(m + 1)}) where A is Element of bool ((Seg (m + 1)) \ {1}) : ( not m + 1 in A & A in bool ((Seg (m + 1)) \ {1}) ) } ) by A10, XBOOLE_0:def 3;

suppose x in { ((A \ {(m + 1)}) \/ {(m + 2)}) where A is Element of bool ((Seg (m + 1)) \ {1}) : m + 1 in A } ; :: thesis: x in bool ((Seg (m + 2)) \ {1})

then consider A being Element of bool ((Seg (m + 1)) \ {1}) such that
A11: ( x = (A \ {(m + 1)}) \/ {(m + 2)} & m + 1 in A ) ;
x c= ((Seg (m + 1)) \ {1}) \/ {(m + 2)} by A11, XBOOLE_1:13;
hence x in bool ((Seg (m + 2)) \ {1}) by A7; :: thesis: verum

end;

suppose x in { (A \/ {(m + 1)}) where A is Element of bool ((Seg (m + 1)) \ {1}) : ( not m + 1 in A & A in bool ((Seg (m + 1)) \ {1}) ) } ; :: thesis: x in bool ((Seg (m + 2)) \ {1})

then consider A being Element of bool ((Seg (m + 1)) \ {1}) such that
A12: ( x = A \/ {(m + 1)} & not m + 1 in A & A in bool ((Seg (m + 1)) \ {1}) ) ;
x c= ((Seg (m + 1)) \ {1}) \/ {(m + 1)} by A12, XBOOLE_1:13;
then x c= (Seg ((m + 1) + 1)) \ {1} by A8, XBOOLE_1:10;
hence x in bool ((Seg (m + 2)) \ {1}) ; :: thesis: verum

end;

end;

end;

Ext ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m)) c= bool ((Seg (m + 2)) \ {1})

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ext ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m)) or x in bool ((Seg (m + 2)) \ {1}) )
assume A13: x in Ext ((bool ((Seg (m + 1)) \ {1})),(1 + m),(2 + m)) ; :: thesis: x in bool ((Seg (m + 2)) \ {1})
reconsider x = x as set by TARSKI:1;

per cases ( x in { (A \/ {(m + 2)}) where A is Element of bool ((Seg (m + 1)) \ {1}) : m + 1 in A } or x in { A where A is Element of bool ((Seg (m + 1)) \ {1}) : ( not m + 1 in A & A in bool ((Seg (m + 1)) \ {1}) ) } ) by A13, XBOOLE_0:def 3;

suppose x in { (A \/ {(m + 2)}) where A is Element of bool ((Seg (m + 1)) \ {1}) : m + 1 in A } ; :: thesis: x in bool ((Seg (m + 2)) \ {1})

then consider A being Element of bool ((Seg (m + 1)) \ {1}) such that
A14: ( x = A \/ {(m + 2)} & m + 1 in A ) ;
x c= ((Seg (m + 1)) \ {1}) \/ {(m + 2)} by A14, XBOOLE_1:13;
hence x in bool ((Seg (m + 2)) \ {1}) by A7; :: thesis: verum

end;

suppose x in { A where A is Element of bool ((Seg (m + 1)) \ {1}) : ( not m + 1 in A & A in bool ((Seg (m + 1)) \ {1}) ) } ; :: thesis: x in bool ((Seg (m + 2)) \ {1})

then consider A being Element of bool ((Seg (m + 1)) \ {1}) such that
A15: ( x = A & not m + 1 in A & A in bool ((Seg (m + 1)) \ {1}) ) ;
x c= ((Seg (m + 1)) \ {1}) \/ {(m + 2)} by A15, XBOOLE_1:10;
hence x in bool ((Seg (m + 2)) \ {1}) by A7; :: thesis: verum

end;

end;

end;

hence 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))) by A5, CARD_2:102, A9, XBOOLE_1:8; :: thesis: verum