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 object ; :: 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 V9 being Subset of FMT such that
A3: V9 in U_FMT y and
A4: V9 c= A by A2, Th21;
V9 c= B by A1, A4;
hence x in B ^Foi by A3; :: thesis: verum