let E be RealLinearSpace; :: thesis: for F being binary-image-family of E
for A being non empty binary-image of E holds A (+) (meet F) c= meet { (A (+) X) where X is binary-image of E : X in F }
let F be binary-image-family of E; :: thesis: for A being non empty binary-image of E holds A (+) (meet F) c= meet { (A (+) X) where X is binary-image of E : X in F }
let A be non empty binary-image of E; :: thesis: A (+) (meet F) c= meet { (A (+) X) where X is binary-image of E : X in F }
A1: for x being object holds
( x in { (X (+) A) where X is binary-image of E : X in F } iff x in { (A (+) X) where X is binary-image of E : X in F } )
proof
let x be object ; :: thesis: ( x in { (X (+) A) where X is binary-image of E : X in F } iff x in { (A (+) X) where X is binary-image of E : X in F } )
hereby :: thesis: ( x in { (A (+) X) where X is binary-image of E : X in F } implies x in { (X (+) A) where X is binary-image of E : X in F } )
assume x in { (X (+) A) where X is binary-image of E : X in F } ; :: thesis: x in { (A (+) X) where X is binary-image of E : X in F }
then consider W being binary-image of E such that
A2: ( x = W (+) A & W in F ) ;
( x = A (+) W & W in F ) by A2;
hence x in { (A (+) X) where X is binary-image of E : X in F } ; :: thesis: verum
end;
assume x in { (A (+) X) where X is binary-image of E : X in F } ; :: thesis: x in { (X (+) A) where X is binary-image of E : X in F }
then consider W being binary-image of E such that
A3: ( x = A (+) W & W in F ) ;
( x = W (+) A & W in F ) by A3;
hence x in { (X (+) A) where X is binary-image of E : X in F } ; :: thesis: verum
end;
A (+) (meet F) c= meet { (X (+) A) where X is binary-image of E : X in F } by Th14;
hence A (+) (meet F) c= meet { (A (+) X) where X is binary-image of E : X in F } by A1, TARSKI:2; :: thesis: verum