set D = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } ;
let c1, c2 be Cardinal; :: thesis: ( c1,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent & c2,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent implies c1 = c2 )
assume that
A1: c1,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent and
A2: c2,{ [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . x,y <= a "\/" b } are_equipotent ; :: thesis: c1 = c2
c1,c2 are_equipotent by A1, A2, WELLORD2:22;
hence c1 = c2 by CARD_1:8; :: thesis: verum