let FMT be non empty FMT_Space_Str ; :: thesis: for A, B being Subset of FMT st A c= B holds
A ^Foi c= B ^Foi
let A, B be Subset of FMT; :: thesis: ( A c= B implies A ^Foi c= B ^Foi )
assume A1: A c= B ; :: thesis: A ^Foi c= B ^Foi
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^Foi or x in B ^Foi )
assume A2: x in A ^Foi ; :: thesis: x in B ^Foi
then reconsider y = x as Element of FMT ;
consider V' being Subset of FMT such that
A3: ( V' in U_FMT y & V' c= A ) by A2, Th22;
( V' in U_FMT y & V' c= B ) by A1, A3, XBOOLE_1:1;
hence x in B ^Foi ; :: thesis: verum