let V be non empty vector-distributive scalar-distributive scalar-associative scalar-unital RLSStruct ; :: thesis: for A being Subset of V holds

( Int A = A iff A is trivial )

let A be Subset of V; :: thesis: ( Int A = A iff A is trivial )

( Int A = A iff A is trivial )

let A be Subset of V; :: thesis: ( Int A = A iff A is trivial )

per cases
( A is empty or not A is empty )
;

end;

suppose A1:
not A is empty
; :: thesis: ( Int A = A iff A is trivial )

then consider v being Element of V such that

A5: A = {v} by A1, SUBSET_1:47;

A6: for B being Subset of V holds

( not B c< A or not v in conv B )

then A9: Int A c= A by Lm2;

v in A by A5, TARSKI:def 1;

then v in Int A by A6, A8, Def1;

hence Int A = A by A5, A9, ZFMISC_1:33; :: thesis: verum

end;

hereby :: thesis: ( A is trivial implies Int A = A )

assume
A is trivial
; :: thesis: Int A = Aassume A2:
Int A = A
; :: thesis: A is trivial

end;now :: thesis: for x, y being object st x in A & y in A holds

x = y

hence
A is trivial
by ZFMISC_1:def 10; :: thesis: verumx = y

let x, y be object ; :: thesis: ( x in A & y in A implies x = y )

assume that

A3: x in A and

A4: y in A ; :: thesis: x = y

( A \ {x} c= A & A \ {x} <> A ) by A3, ZFMISC_1:56;

then ( A \ {x} c= conv (A \ {x}) & A \ {x} c< A ) by RLAFFIN1:2;

then not y in A \ {x} by A2, Def1;

hence x = y by A4, ZFMISC_1:56; :: thesis: verum

end;assume that

A3: x in A and

A4: y in A ; :: thesis: x = y

( A \ {x} c= A & A \ {x} <> A ) by A3, ZFMISC_1:56;

then ( A \ {x} c= conv (A \ {x}) & A \ {x} c< A ) by RLAFFIN1:2;

then not y in A \ {x} by A2, Def1;

hence x = y by A4, ZFMISC_1:56; :: thesis: verum

then consider v being Element of V such that

A5: A = {v} by A1, SUBSET_1:47;

A6: for B being Subset of V holds

( not B c< A or not v in conv B )

proof

A8:
conv A = A
by A5, RLAFFIN1:1;
let B be Subset of V; :: thesis: ( not B c< A or not v in conv B )

assume A7: B c< A ; :: thesis: not v in conv B

B is empty by A5, A7, ZFMISC_1:33;

hence not v in conv B ; :: thesis: verum

end;assume A7: B c< A ; :: thesis: not v in conv B

B is empty by A5, A7, ZFMISC_1:33;

hence not v in conv B ; :: thesis: verum

then A9: Int A c= A by Lm2;

v in A by A5, TARSKI:def 1;

then v in Int A by A6, A8, Def1;

hence Int A = A by A5, A9, ZFMISC_1:33; :: thesis: verum