thus 2Set (Seg 0) = {} :: thesis: 2Set (Seg 1) = {}

proof

assume 2Set (Seg 0) <> {} ; :: thesis: contradiction
then consider x being set such that
A1: x in 2Set (Seg 0) by XBOOLE_0:def 1;
ex i, j being Nat st
( i in Seg 0 & j in Seg 0 & i < j & x = {i,j} ) by A1, Th1;
hence contradiction ; :: thesis: verum

end;

thus 2Set (Seg 1) = {} :: thesis: verum

proof

assume 2Set (Seg 1) <> {} ; :: thesis: contradiction
then consider x being set such that
A2: x in 2Set (Seg 1) by XBOOLE_0:def 1;
consider i, j being Nat such that
A3: i in Seg 1 and
A4: j in Seg 1 and
A5: i < j and
x = {i,j} by A2, Th1;
i = 1 by A3, FINSEQ_1:2, TARSKI:def 1;
hence contradiction by A4, A5, FINSEQ_1:2, TARSKI:def 1; :: thesis: verum

end;