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

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