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 ;
TARSKI:def 3 ( not z in rng f or z in [:A,A, the carrier of L, the carrier of L:] )
assume
z in rng f
;
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:]
;
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
; ( 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; ( 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; 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; verum