let Omega be non empty set ; :: thesis:
let Sigma be SigmaField of Omega; :: thesis:
let I be non empty real-membered set ; :: thesis:
assume A0: ( I = {1,2,3} & Sigma = bool {1,2,3,4} & Omega = {1,2,3,4} ) ; :: thesis:
consider MyFunc being ManySortedSigmaField of I,Sigma such that
A1: ( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} ) by A0, Th3;
A3: for s, t being Element of I st s <= t holds
MyFunc . s is Subset of (MyFunc . t)

proof

let s, t be Element of I; :: thesis:
assume B1: s <= t ; :: thesis:

per cases by A0, ENUMSET1:def 1;

suppose SUPP1: s = 1 ; :: thesis:

per cases by A0, ENUMSET1:def 1;

suppose t = 1 ; :: thesis:

then ( MyFunc . t = MyFunc . 1 & MyFunc . s = MyFunc . 1 ) by SUPP1;
hence MyFunc . s is Subset of (MyFunc . t) ; :: thesis:

end;

suppose ( t = 2 or t = 3 ) ; :: thesis:

hence MyFunc . s is Subset of (MyFunc . t) by SUPP1, A1, XX1; :: thesis:

end;

end;

end;

suppose SUPP1: s = 2 ; :: thesis:

per cases by A0, ENUMSET1:def 1;

suppose t = 1 ; :: thesis:

hence MyFunc . s is Subset of (MyFunc . t) by SUPP1, B1; :: thesis:

end;

suppose t = 2 ; :: thesis:

then ( MyFunc . t = MyFunc . 2 & MyFunc . s = MyFunc . 2 ) by SUPP1;
hence MyFunc . s is Subset of (MyFunc . t) ; :: thesis:

end;

suppose t = 3 ; :: thesis:

hence MyFunc . s is Subset of (MyFunc . t) by SUPP1, A1; :: thesis:

end;

end;

end;

suppose SUPP1: s = 3 ; :: thesis:

per cases by A0, ENUMSET1:def 1;

suppose ( t = 1 or t = 2 ) ; :: thesis:

hence MyFunc . s is Subset of (MyFunc . t) by SUPP1, B1; :: thesis:

end;

suppose t = 3 ; :: thesis:

then ( MyFunc . t = MyFunc . 3 & MyFunc . s = MyFunc . 3 ) by SUPP1;
hence MyFunc . s is Subset of (MyFunc . t) ; :: thesis:

end;

end;

end;

end;

end;

MyFunc is Filtration of I,Sigma by A3, Def2000;
hence ex MyFunc being Filtration of I,Sigma st
( MyFunc . 1 = Special_SigmaField1 & MyFunc . 2 = Special_SigmaField2 & MyFunc . 3 = Trivial-SigmaField {1,2,3,4} ) by A1; :: thesis: