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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in mi (A ^ B) or a in A )
reconsider aa = a as set by TARSKI:1;
A3: A c= PFuncs (V,C) by FINSUB_1:def 5;
assume A4: a in mi (A ^ B) ; :: thesis: a in A
then consider b, c being set such that
A5: b in A and
c in B and
A6: a = b \/ c by A2, SUBSTLAT:15;
A7: b c= aa by A6, XBOOLE_1:7;
consider b1 being set such that
A8: b1 in B and
A9: b1 c= b by A1, A5;
B c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider b9 = b, b19 = b1 as Element of PFuncs (V,C) by A5, A8, A3;
A10: b = b1 \/ b by A9, XBOOLE_1:12;
b19 tolerates b9 by A9, PARTFUN1:54;
then b in A ^ B by A5, A8, A10, SUBSTLAT:16;
hence a in A by A4, A5, A7, SUBSTLAT:6; :: thesis: verum

end;

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

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in A or a in mi (A ^ B) )
reconsider aa = a as set by TARSKI:1;
A11: A c= PFuncs (V,C) by FINSUB_1:def 5;
assume A12: a in A ; :: thesis: a in mi (A ^ B)
then consider b being set such that
A13: b in B and
A14: b c= aa by A1;
B c= PFuncs (V,C) by FINSUB_1:def 5;
then reconsider a9 = a, b9 = b as Element of PFuncs (V,C) by A12, A13, A11;
A15: a9 tolerates b9 by A14, PARTFUN1:54;
A16: a in mi A by A12, SUBSTLAT:11;
A17: for b being finite set st b in A ^ B & b c= aa holds
b = a

proof

let b be finite set ; :: thesis: ( b in A ^ B & b c= aa implies b = a )
assume that
A18: b in A ^ B and
A19: b c= aa ; :: thesis: b = a
consider c, d being set such that
A20: c in A and
d in B and
A21: b = c \/ d by A18, SUBSTLAT:15;
c c= b by A21, XBOOLE_1:7;
then c c= aa by A19;
then c = a by A16, A20, SUBSTLAT:6;
hence b = a by A19, A21, Lm1; :: thesis: verum

end;

a9 = a9 \/ b9 by A14, XBOOLE_1:12;
then A22: a9 in A ^ B by A12, A13, A15, SUBSTLAT:16;
aa is finite by A12, Th1;
hence a in mi (A ^ B) by A22, A17, SUBSTLAT:7; :: thesis: verum

end;