let x be set ; :: according to MEMBERED:def 6 :: thesis: ( not x in the carrier of dL-Z_2 or not x is V27() )
thus ( not x in the carrier of dL-Z_2 or not x is V27() ) by CARD_1:50, TARSKI:def 2; :: thesis: verum