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
A3: ( b in A & c in B & 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, XBOOLE_1:7; :: thesis: verum