let V be set ; :: thesis: for C being finite set
for u, v being Element of (SubstLatt (V,C)) st v in SUB u holds
v "\/" ((diff u) . v) = u
let C be finite set ; :: thesis: for u, v being Element of (SubstLatt (V,C)) st v in SUB u holds
v "\/" ((diff u) . v) = u
let u, v be Element of (SubstLatt (V,C)); :: thesis: ( v in SUB u implies v "\/" ((diff u) . v) = u )
assume A1: v in SUB u ; :: thesis: v "\/" ((diff u) . v) = u
reconsider u9 = u, v9 = v, dv = (diff u) . v as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
A2: u \ v = (diff u) . v by Def7;
thus v "\/" ((diff u) . v) = the L_join of (SubstLatt (V,C)) . (v,((diff u) . v)) by LATTICES:def 1
.= mi (v9 \/ dv) by SUBSTLAT:def 4
.= mi u9 by A1, A2, XBOOLE_1:45
.= u by SUBSTLAT:11 ; :: thesis: verum