let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } or x in the carrier of L )
assume x in { ("/\" (Y,L)) where Y is finite Subset of X : ex_inf_of Y,L } ; :: thesis: x in the carrier of L
then ex Y being finite Subset of X st
( x = "/\" (Y,L) & ex_inf_of Y,L ) ;
hence x in the carrier of L ; :: thesis: verum