let A be non empty set ; :: thesis: for L being lower-bounded LATTICE
for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds
( O in DistEsti d iff O in dom q )
let L be lower-bounded LATTICE; :: thesis: for O being Ordinal
for d being BiFunction of A,L
for q being QuadrSeq of d holds
( O in DistEsti d iff O in dom q )
let O be Ordinal; :: thesis: for d being BiFunction of A,L
for q being QuadrSeq of d holds
( O in DistEsti d iff O in dom q )
let d be BiFunction of A,L; :: thesis: for q being QuadrSeq of d holds
( O in DistEsti d iff O in dom q )
let q be QuadrSeq of d; :: thesis: ( O in DistEsti d iff O in dom q )
reconsider N = dom q as Cardinal by Def13;
reconsider M = DistEsti d as Cardinal ;
q is one-to-one by Def13;
then A1: dom q, rng q are_equipotent by WELLORD2:def 4;
DistEsti d, { [x,y,a,b] where x, y is Element of A, a, b is Element of L : d . (x,y) <= a "\/" b } are_equipotent by Def11;
then DistEsti d, rng q are_equipotent by Def13;
then DistEsti d, dom q are_equipotent by A1, WELLORD2:15;
then A2: M = N by CARD_1:2;
hence ( O in DistEsti d implies O in dom q ) ; :: thesis: ( O in dom q implies O in DistEsti d )
assume O in dom q ; :: thesis: O in DistEsti d
hence O in DistEsti d by A2; :: thesis: verum