set D = the non empty set ;
set Z = the Element of the non empty set ;
set a = the BinOp of the non empty set ;
set m = the Function of [: the carrier of F, the non empty set :], the non empty set ;
set s = the Function of [: the non empty set , the non empty set :], the carrier of F_Real;
take LatticeStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :], the carrier of F_Real #) ; :: thesis: ( LatticeStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :], the carrier of F_Real #) is strict & not LatticeStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :], the carrier of F_Real #) is empty )
thus ( LatticeStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :], the carrier of F_Real #) is strict & not LatticeStr(# the non empty set , the BinOp of the non empty set , the Element of the non empty set , the Function of [: the carrier of F, the non empty set :], the non empty set , the Function of [: the non empty set , the non empty set :], the carrier of F_Real #) is empty ) ; :: thesis: verum