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