let V, C be set ; :: thesis: for A, B being Element of SubstitutionSet V,C st ( for a being set st a in A holds
ex b being set st
( b in B & b c= a ) ) holds
mi (A ^ B) = A
let A, B be Element of SubstitutionSet V,C; :: thesis: ( ( for a being set st a in A holds
ex b being set st
( b in B & b c= a ) ) implies mi (A ^ B) = A )
assume A1: for a being set st a in A holds
ex b being set st
( b in B & b c= a ) ; :: thesis: mi (A ^ B) = A
A2: mi (A ^ B) c= A ^ B by SUBSTLAT:8;
thus mi (A ^ B) c= A :: according to XBOOLE_0:def 10 :: thesis: A c= mi (A ^ B)

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in mi (A ^ B) or a in A )
assume A3: a in mi (A ^ B) ; :: thesis: a in A
then consider b, c being set such that
A4: ( b in A & c in B & a = b \/ c ) by A2, SUBSTLAT:15;
consider b1 being set such that
A5: ( b1 in B & b1 c= b ) by A1, A4;
( B c= PFuncs V,C & A c= PFuncs V,C ) by FINSUB_1:def 5;
then reconsider b' = b, b1' = b1 as Element of PFuncs V,C by A4, A5;
A6: b1' tolerates b' by A5, PARTFUN1:135;
b = b1 \/ b by A5, XBOOLE_1:12;
then A7: b in A ^ B by A4, A5, A6, SUBSTLAT:16;
b c= a by A4, XBOOLE_1:7;
hence a in A by A3, A4, A7, SUBSTLAT:6; :: thesis: verum

end;

thus A c= mi (A ^ B) :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in mi (A ^ B) )
assume A8: a in A ; :: thesis: a in mi (A ^ B)
then consider b being set such that
A9: ( b in B & b c= a ) by A1;
A10: a in mi A by A8, SUBSTLAT:11;
A11: a is finite by A8, Th2;
( B c= PFuncs V,C & A c= PFuncs V,C ) by FINSUB_1:def 5;
then reconsider a' = a, b' = b as Element of PFuncs V,C by A8, A9;
A12: a' = a' \/ b' by A9, XBOOLE_1:12;
a' tolerates b' by A9, PARTFUN1:135;
then A13: a' in A ^ B by A8, A9, A12, SUBSTLAT:16;
for b being finite set st b in A ^ B & b c= a holds
b = a

proof

let b be finite set ; :: thesis: ( b in A ^ B & b c= a implies b = a )
assume A14: ( b in A ^ B & b c= a ) ; :: thesis: b = a
then consider c, d being set such that
A15: ( c in A & d in B & b = c \/ d ) by SUBSTLAT:15;
c c= b by A15, XBOOLE_1:7;
then c c= a by A14, XBOOLE_1:1;
then c = a by A10, A15, SUBSTLAT:6;
hence b = a by A14, A15, Lm1; :: thesis: verum

end;

hence a in mi (A ^ B) by A11, A13, SUBSTLAT:7; :: thesis: verum

end;