set x = { i where i is Element of NAT : i < 4 } ;
A1: { i where i is Element of NAT : i < 4 } c= {0 ,1,2,3}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { i where i is Element of NAT : i < 4 } or y in {0 ,1,2,3} )
assume y in { i where i is Element of NAT : i < 4 } ; :: thesis: y in {0 ,1,2,3}
then consider i being Element of NAT such that
A2: ( y = i & i < 3 + 1 ) ;
i <= 3 by A2, NAT_1:13;
then ( i = 0 or i = 1 or i = 2 or i = 3 ) by NAT_1:28;
hence y in {0 ,1,2,3} by A2, ENUMSET1:def 2; :: thesis: verum

end;

A3: {0 ,1,2,3} c= { i where i is Element of NAT : i < 4 }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {0 ,1,2,3} or y in { i where i is Element of NAT : i < 4 } )
assume y in {0 ,1,2,3} ; :: thesis: y in { i where i is Element of NAT : i < 4 }
then ( y = 0 or y = 1 or y = 2 or y = 3 ) by ENUMSET1:def 2;
hence y in { i where i is Element of NAT : i < 4 } ; :: thesis: verum

end;

thus 4 = { i where i is Element of NAT : i < 4 } by AXIOMS:30
.= {0 ,1,2,3} by A1, A3, XBOOLE_0:def 10 ; :: thesis: verum