consider D being non empty set , m being BinOp of D, c being Relation of [:D,D:];
take AfMidStruct(# D,m,c #) ; :: thesis: ( not AfMidStruct(# D,m,c #) is empty & AfMidStruct(# D,m,c #) is strict )
thus not the carrier of AfMidStruct(# D,m,c #) is empty ; :: according to STRUCT_0:def 1 :: thesis: AfMidStruct(# D,m,c #) is strict
thus AfMidStruct(# D,m,c #) is strict ; :: thesis: verum