let e be object ; :: according to TARSKI:def 3:: thesis: ( not e in { H1(k) where k is Nat : S3[k] } or e in { H1(n) where n is Nat : S2[n] } ) assume
e in { H1(k) where k is Nat : S3[k] }
; :: thesis: e in { H1(n) where n is Nat : S2[n] } then
ex k being Nat st ( e = H1(k) & S3[k] )
; hence
e in { H1(n) where n is Nat : S2[n] }
; :: thesis: verum