let FT be non empty RelStr ; :: thesis: for A, B being Subset of FT st A c= B holds
A ^b c= B ^b
let A, B be Subset of FT; :: thesis: ( A c= B implies A ^b c= B ^b )
assume A1: A c= B ; :: thesis: A ^b c= B ^b
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A ^b or x in B ^b )
assume A2: x in A ^b ; :: thesis: x in B ^b
then reconsider y = x as Element of FT ;
U_FT y meets A by A2, Th8;
then ex w being object st
( w in U_FT y & w in A ) by XBOOLE_0:3;
then U_FT y meets B by A1, XBOOLE_0:3;
hence x in B ^b ; :: thesis: verum