now 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 ;
( 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 }
;
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]
;
verum end;
hence
{ [a,b] where a, b is Element of L : a "/\" b = b } is Relation
by RELAT_1:def 1; verum