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

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

hence
x in B ^Fob
; :: thesis: verum
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;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