consider S being Scott TopAugmentation of L1;
A1: RelStr(# the carrier of S,the InternalRel of S #) = RelStr(# the carrier of L1,the InternalRel of L1 #) by YELLOW_9:def 4;
InclPoset (sigma S) is complete ;
hence InclPoset (sigma L1) is with_suprema by A1, YELLOW_9:52; :: thesis: InclPoset (sigma L1) is continuous
InclPoset (sigma S) is continuous by WAYBEL14:36;
hence InclPoset (sigma L1) is continuous by A1, YELLOW_9:52; :: thesis: verum