let x be set ; :: 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