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