{ x where x is Element of X : ex y being Element of X st

( x,y in O & x in L ) } c= X

( x,y in O & x in L ) } is List of X ; :: thesis: verum

( x,y in O & x in L ) } c= X

proof

hence
{ x where x is Element of X : ex y being Element of X st
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in { x where x is Element of X : ex y being Element of X st

( x,y in O & x in L ) } or z in X )

assume z in { x where x is Element of X : ex y being Element of X st

( x,y in O & x in L ) } ; :: thesis: z in X

then consider x being Element of X such that

A7: ( z = x & ex y being Element of X st

( x,y in O & x in L ) ) ;

thus z in X by A7; :: thesis: verum

end;( x,y in O & x in L ) } or z in X )

assume z in { x where x is Element of X : ex y being Element of X st

( x,y in O & x in L ) } ; :: thesis: z in X

then consider x being Element of X such that

A7: ( z = x & ex y being Element of X st

( x,y in O & x in L ) ) ;

thus z in X by A7; :: thesis: verum

( x,y in O & x in L ) } is List of X ; :: thesis: verum