let RLS be non empty RLSStruct ; :: thesis: for A, B being Subset of RLS st A c= B holds

conv A c= conv B

let A, B be Subset of RLS; :: thesis: ( A c= B implies conv A c= conv B )

assume A1: A c= B ; :: thesis: conv A c= conv B

A2: Convex-Family B c= Convex-Family A

then [#] RLS in Convex-Family B by CONVEX1:def 4;

then A5: meet (Convex-Family A) c= meet (Convex-Family B) by A2, SETFAM_1:6;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in conv A or y in conv B )

assume y in conv A ; :: thesis: y in conv B

hence y in conv B by A5; :: thesis: verum

conv A c= conv B

let A, B be Subset of RLS; :: thesis: ( A c= B implies conv A c= conv B )

assume A1: A c= B ; :: thesis: conv A c= conv B

A2: Convex-Family B c= Convex-Family A

proof

[#] RLS is convex
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Convex-Family B or x in Convex-Family A )

assume A3: x in Convex-Family B ; :: thesis: x in Convex-Family A

then reconsider X = x as Subset of RLS ;

B c= X by A3, CONVEX1:def 4;

then A4: A c= X by A1;

X is convex by A3, CONVEX1:def 4;

hence x in Convex-Family A by A4, CONVEX1:def 4; :: thesis: verum

end;assume A3: x in Convex-Family B ; :: thesis: x in Convex-Family A

then reconsider X = x as Subset of RLS ;

B c= X by A3, CONVEX1:def 4;

then A4: A c= X by A1;

X is convex by A3, CONVEX1:def 4;

hence x in Convex-Family A by A4, CONVEX1:def 4; :: thesis: verum

then [#] RLS in Convex-Family B by CONVEX1:def 4;

then A5: meet (Convex-Family A) c= meet (Convex-Family B) by A2, SETFAM_1:6;

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in conv A or y in conv B )

assume y in conv A ; :: thesis: y in conv B

hence y in conv B by A5; :: thesis: verum