consider M being ManySortedSet of ;
take A = AltGraph(# 1,M #); :: thesis: ( not A is empty & A is strict )
thus not the carrier of A is empty ; :: according to STRUCT_0:def 1 :: thesis: A is strict
thus A is strict ; :: thesis: verum