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