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 }
; 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 2; verum