H: INT.Ring 2 = doubleLoopStr(# (Segm 2),(addint 2),(multint 2),(In (1,(Segm 2))),(In (0,(Segm 2))) #) by INT_3:def 12;
I: ( In (1,(Segm 2)) = 1 & In (0,(Segm 2)) = 0 ) by NAT_1:44, SUBSET_1:def 8;

A: now :: thesis: for o being object st o in the carrier of (Z/ 2) holds
o in {(0. (Z/ 2)),(1. (Z/ 2))}

let o be object ; :: thesis: ( o in the carrier of (Z/ 2) implies b₁ in {(0. (Z/ 2)),(1. (Z/ 2))} )
assume A1: o in the carrier of (Z/ 2) ; :: thesis: b₁ in {(0. (Z/ 2)),(1. (Z/ 2))}
then reconsider k = o as Nat by H;

per cases ( k = 0 or k = 1 ) by H, A1, NAT_1:44, NAT_1:23;

suppose k = 0 ; :: thesis: b₁ in {(0. (Z/ 2)),(1. (Z/ 2))}

hence o in {(0. (Z/ 2)),(1. (Z/ 2))} by I, H, TARSKI:def 2; :: thesis: verum

end;

suppose k = 1 ; :: thesis: b₁ in {(0. (Z/ 2)),(1. (Z/ 2))}

hence o in {(0. (Z/ 2)),(1. (Z/ 2))} by I, H, TARSKI:def 2; :: thesis: verum

end;

end;

end;

for o being object st o in {(0. (Z/ 2)),(1. (Z/ 2))} holds
o in the carrier of (Z/ 2) ;
hence the carrier of (Z/ 2) = {(0. (Z/ 2)),(1. (Z/ 2))} by A, TARSKI:2; :: thesis: verum