set M = the ManySortedSet of [:1,1:];
take A = AltGraph(# 1, the ManySortedSet of [:1,1:] #); :: 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