now :: thesis: for x being object st x in { [p,q] where p, q is Element of L : p "/\" q = q } holds
ex x1, x2 being object st x = [x1,x2]

let x be object ; :: thesis: ( x in { [p,q] where p, q is Element of L : p "/\" q = q } implies ex x1, x2 being object st x = [x1,x2] )
assume x in { [p,q] where p, q is Element of L : p "/\" q = q } ; :: thesis: ex x1, x2 being object st x = [x1,x2]
then ex p, q being Element of L st
( x = [p,q] & p "/\" q = q ) ;
hence ex x1, x2 being object st x = [x1,x2] ; :: thesis: verum

end;

hence { [a,b] where a, b is Element of L : a "/\" b = b } is Relation by RELAT_1:def 1; :: thesis: verum