let L1 be lower-bounded continuous sup-Semilattice; :: thesis: for T being Scott TopAugmentation of L1
for B1 being Basis of T st not B1 is finite holds
not { (inf u) where u is Subset of T : u in B1 } is finite
let T be Scott TopAugmentation of L1; :: thesis: for B1 being Basis of T st not B1 is finite holds
not { (inf u) where u is Subset of T : u in B1 } is finite
let B1 be Basis of T; :: thesis: ( not B1 is finite implies not { (inf u) where u is Subset of T : u in B1 } is finite )
assume that
A1: not B1 is finite and
A2: { (inf u) where u is Subset of T : u in B1 } is finite ; :: thesis: contradiction
reconsider B2 = { (inf u) where u is Subset of T : u in B1 } as set ;
reconsider B3 = { (wayabove (inf u)) where u is Subset of T : u in B1 } as Basis of T by Th27;
defpred S₁[ set , set ] means ex y being Element of T st
( $1 = y & $2 = wayabove y );
A3: for x being set st x in B2 holds
ex y being set st
( y in B3 & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in B2 implies ex y being set st
( y in B3 & S₁[x,y] ) )
assume x in B2 ; :: thesis: ex y being set st
( y in B3 & S₁[x,y] )
then consider u1 being Subset of T such that
A4: x = inf u1 and
A5: u1 in B1 ;
reconsider z = x as Element of T by A4;
take y = wayabove z; :: thesis: ( y in B3 & S₁[x,y] )
thus y in B3 by A4, A5; :: thesis: S₁[x,y]
take z ; :: thesis: ( x = z & y = wayabove z )
thus ( x = z & y = wayabove z ) ; :: thesis: verum

end;

consider f being Function such that
A6: dom f = B2 and
A7: rng f c= B3 and
A8: for x being set st x in B2 holds
S₁[x,f . x] from WELLORD2:sch 1(A3);
B3 c= rng f

proof

let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in B3 or z in rng f )
assume z in B3 ; :: thesis: z in rng f
then consider u1 being Subset of T such that
A9: z = wayabove (inf u1) and
A10: u1 in B1 ;
inf u1 in B2 by A10;
then consider y being Element of T such that
A11: inf u1 = y and
A12: f . (inf u1) = wayabove y by A8;
( z = f . (inf u1) & inf u1 in B2 ) by A9, A10, A11, A12;
hence z in rng f by A6, FUNCT_1:def 5; :: thesis: verum

end;

then rng f = B3 by A7, XBOOLE_0:def 10;
then B3 is finite by A2, A6, FINSET_1:26;
then T is finite by YELLOW15:31;
then the carrier of T is finite ;
hence contradiction by A1; :: thesis: verum