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

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