now :: thesis: for x being object st x in { [p,q] where p, q is Element of L : p [= q } holds

ex x1, x2 being object st x = [x1,x2]

hence
{ [p,q] where p, q is Element of L : p [= q } is Relation
by RELAT_1:def 1; :: thesis: verumex 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 } implies ex x1, x2 being object st x = [x1,x2] )

assume x in { [p,q] where p, q is Element of L : p [= 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 ) ;

hence ex x1, x2 being object st x = [x1,x2] ; :: thesis: verum

end;assume x in { [p,q] where p, q is Element of L : p [= 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 ) ;

hence ex x1, x2 being object st x = [x1,x2] ; :: thesis: verum