let T be non empty RelStr ; :: thesis: for A, B being Subset of T st A c= B holds
A ^f c= B ^f
let A, B be Subset of T; :: thesis: ( A c= B implies A ^f c= B ^f )
assume A1: A c= B ; :: thesis: A ^f c= B ^f
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in A ^f or z in B ^f )
assume z in A ^f ; :: thesis: z in B ^f
then ex y being Element of T st
( y in A & z in U_FT y ) by FIN_TOPO:11;
hence z in B ^f by A1, FIN_TOPO:11; :: thesis: verum