let FMT be non empty FMT_Space_Str ; :: thesis: for A, B being Subset of FMT st A c= B holds
A ^Fob c= B ^Fob
let A, B be Subset of FMT; :: thesis: ( A c= B implies A ^Fob c= B ^Fob )
assume A1: A c= B ; :: thesis: A ^Fob c= B ^Fob
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^Fob or x in B ^Fob )
assume A2: x in A ^Fob ; :: thesis: x in B ^Fob
then reconsider y = x as Element of FMT ;
for W being Subset of FMT st W in U_FMT y holds
W meets B

proof

let W be Subset of FMT; :: thesis: ( W in U_FMT y implies W meets B )
assume W in U_FMT y ; :: thesis: W meets B
then W meets A by A2, Th20;
then ex z being object st
( z in W & z in A ) by XBOOLE_0:3;
hence W /\ B <> {} by A1, XBOOLE_0:def 4; :: according to XBOOLE_0:def 7 :: thesis: verum

end;

hence x in B ^Fob ; :: thesis: verum