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 5;
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 T-Sequence by A2, ORDINAL1:def 7;
rng f c= [:A,A,the carrier of L,the carrier of L:]

proof

let z be set ; :: 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 consider x, y being Element of A, a, b being Element of L such that
A4: ( z = [x,y,a,b] & d . x,y <= a "\/" b ) by A3;
thus z in [:A,A,the carrier of L,the carrier of L:] by A4; :: thesis: verum

end;

then reconsider f = f as T-Sequence of 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