let V, C be set ; :: thesis: 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); :: thesis: ( 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 ; :: thesis: for a being set st a in A holds
ex b being set st
( b in B & b c= a )
let a be set ; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( c in B & c c= a )
thus ( c in B & c c= a ) by A3, A4, XBOOLE_1:7; :: thesis: verum