now :: thesis: for x being object st x in { [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p) } holds
x in [: the carrier of (GF p), the carrier of (GF p):]

let x be object ; :: thesis: ( x in { [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p) } implies x in [: the carrier of (GF p), the carrier of (GF p):] )
assume x in { [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p) } ; :: thesis: x in [: the carrier of (GF p), the carrier of (GF p):]
then ex a, b being Element of (GF p) st
( x = [a,b] & Disc (a,b,p) <> 0. (GF p) ) ;
hence x in [: the carrier of (GF p), the carrier of (GF p):] ; :: thesis: verum

end;

hence { [a,b] where a, b is Element of (GF p) : Disc (a,b,p) <> 0. (GF p) } is Subset of [: the carrier of (GF p), the carrier of (GF p):] by TARSKI:def 3; :: thesis: verum