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