set D = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } ;
take card { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } ; :: thesis: card { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } ,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent
thus card { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } ,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent by CARD_1:def 5; :: thesis: verum