thus
weight Sorgenfrey-line c= continuum
by Lm5, Lm6, Th20, WAYBEL23:73; :: according to XBOOLE_0:def 10 :: thesis: 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 ; :: thesis: 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; :: thesis: verum

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 ; :: thesis: 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; :: thesis: verum