thus
weight Sorgenfrey-line c= continuum
by Lm5, Lm6, Th20, WAYBEL23:73; XBOOLE_0:def 10 continuum c= weight Sorgenfrey-line
consider B being Basis of Sorgenfrey-line such that
A1:
weight Sorgenfrey-line = card B
by WAYBEL23:74;
assume
not continuum c= weight Sorgenfrey-line
; contradiction
then A2:
weight Sorgenfrey-line in continuum
by CARD_1:4;
the carrier of Sorgenfrey-line = REAL
by Def2;
then consider x being Real, q being Rational such that
x < q
and
A3:
not [.x,q.[ in UniCl B
by A2, A1, Th32;
[.x,q.[ is open Subset of Sorgenfrey-line
by Th11;
then
[.x,q.[ in the topology of Sorgenfrey-line
by PRE_TOPC:def 2;
hence
contradiction
by A3, YELLOW_9:22; verum