let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S
for x being set holds
( x is MinTerm of S,X iff x in MinTerms X )
let X be non-empty ManySortedSet of S; :: thesis: for x being set holds
( x is MinTerm of S,X iff x in MinTerms X )
let x be set ; :: thesis: ( x is MinTerm of S,X iff x in MinTerms X )

hereby :: thesis: ( x in MinTerms X implies x is MinTerm of S,X )

assume x is MinTerm of S,X ; :: thesis: x in MinTerms X
then reconsider t = x as MinTerm of S,X ;
(PTMin X) . t = t by Def32;
hence x in MinTerms X by FUNCT_2:4; :: thesis: verum

end;

assume x in MinTerms X ; :: thesis: x is MinTerm of S,X
then consider y being object such that
A1: y in dom (PTMin X) and
A2: x = (PTMin X) . y by FUNCT_1:def 3;
reconsider t = y as Element of TS (DTConOSA X) by A1;
(PTMin X) . t is Element of TS (DTConOSA X) ;
then reconsider tx = x as Element of TS (DTConOSA X) by A2;
(PTMin X) . tx = tx by A1, A2, Th43;
hence x is MinTerm of S,X by Def32; :: thesis: verum