let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { y where y is Element of L : [y,x] in AR } or z in the carrier of L )
assume z in { y where y is Element of L : [y,x] in AR } ; :: thesis: z in the carrier of L
then ex y being Element of L st
( z = y & [y,x] in AR ) ;
hence z in the carrier of L ; :: thesis: verum