let S be monotone regular locally_directed OrderSortedSign; :: thesis: for X being V2() ManySortedSet of S
for x being set holds
( x is MinTerm of S,X iff x in MinTerms X )
let X be V2() 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