let V, C be set ; for A, B being Element of SubstitutionSet (V,C) st mi (A ^ B) = A holds
for a being set st a in A holds
ex b being set st
( b in B & b c= a )
let A, B be Element of SubstitutionSet (V,C); ( mi (A ^ B) = A implies for a being set st a in A holds
ex b being set st
( b in B & b c= a ) )
assume A1:
mi (A ^ B) = A
; for a being set st a in A holds
ex b being set st
( b in B & b c= a )
let a be set ; ( a in A implies ex b being set st
( b in B & b c= a ) )
A2:
mi (A ^ B) c= A ^ B
by SUBSTLAT:8;
assume
a in A
; ex b being set st
( b in B & b c= a )
then consider b, c being set such that
b in A
and
A3:
c in B
and
A4:
a = b \/ c
by A1, A2, SUBSTLAT:15;
take
c
; ( c in B & c c= a )
thus
( c in B & c c= a )
by A3, A4, XBOOLE_1:7; verum