set L = BoolePoset {0};
set T = the Scott TopAugmentation of BoolePoset {0};
take the Scott TopAugmentation of BoolePoset {0} ; :: thesis: ( not the Scott TopAugmentation of BoolePoset {0} is trivial & the Scott TopAugmentation of BoolePoset {0} is complete & the Scott TopAugmentation of BoolePoset {0} is Scott )
( BoolePoset {0} = InclPoset (bool {0}) & RelStr(# the carrier of the Scott TopAugmentation of BoolePoset {0}, the InternalRel of the Scott TopAugmentation of BoolePoset {0} #) = RelStr(# the carrier of (BoolePoset {0}), the InternalRel of (BoolePoset {0}) #) ) by YELLOW_1:4, YELLOW_9:def 4;
then A1: the carrier of the Scott TopAugmentation of BoolePoset {0} = bool {0} by YELLOW_1:1;
( 0 in {0,1} & 1 in {0,1} ) by TARSKI:def 2;
hence ( not the Scott TopAugmentation of BoolePoset {0} is trivial & the Scott TopAugmentation of BoolePoset {0} is complete & the Scott TopAugmentation of BoolePoset {0} is Scott ) by A1, YELLOW14:1; :: thesis: verum