set X = { [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 by CARD_1:def 2;
then consider f being Function such that
A1: f is one-to-one and
A2: dom f = card { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } and
A3: rng f = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } by WELLORD2:def 4;
reconsider f = f as Sequence by A2, ORDINAL1:def 7;
rng f c= [:A,A, the carrier of L, the carrier of L:]

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng f or z in [:A,A, the carrier of L, the carrier of L:] )
assume z in rng f ; :: thesis: z in [:A,A, the carrier of L, the carrier of L:]
then ex x, y being Element of A ex a, b being Element of L st
( z = [x,y,a,b] & d . (x,y) <= a "\/" b ) by A3;
hence z in [:A,A, the carrier of L, the carrier of L:] ; :: thesis: verum

end;

then reconsider f = f as Sequence of [:A,A, the carrier of L, the carrier of L:] by RELAT_1:def 19;
take f ; :: thesis: ( dom f is Cardinal & f is one-to-one & rng f = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } )
thus dom f is Cardinal by A2; :: thesis: ( f is one-to-one & rng f = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } )
thus f is one-to-one by A1; :: thesis: rng f = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b }
thus rng f = { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } by A3; :: thesis: verum