let x be object ; :: thesis: ( x in INT.Group 2 iff ( x = 0 or x = 1 ) )
thus ( not x in INT.Group 2 or x = 0 or x = 1 ) :: thesis: ( ( x = 0 or x = 1 ) implies x in INT.Group 2 )

proof

assume x in INT.Group 2 ; :: thesis: ( x = 0 or x = 1 )
then x in Segm 2 by Th76;
hence ( x = 0 or x = 1 ) by CARD_1:50, TARSKI:def 2; :: thesis: verum

end;

assume ( x = 0 or x = 1 ) ; :: thesis: x in INT.Group 2
then x in Segm 2 by CARD_1:50, TARSKI:def 2;
hence x in INT.Group 2 by Th76; :: thesis: verum