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