let I be I_Lattice; :: thesis: for i, j being Element of I
for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds
i => j in <.DI.)
let i, j be Element of I; :: thesis: for DI being non empty Subset of I st j in <.(DI \/ {i}).) holds
i => j in <.DI.)
let DI be non empty Subset of I; :: thesis: ( j in <.(DI \/ {i}).) implies i => j in <.DI.) )
assume A1: j in <.(DI \/ {i}).) ; :: thesis: i => j in <.DI.)
<.(DI \/ {i}).) = <.(<.DI.) \/ {i}).) by Th34
.= <.(<.DI.) \/ <.{i}.)).) by Th34
.= <.(<.DI.) \/ <.i.)).) by Th24
.= <.DI.) "/\" <.i.) by Th38 ;
then consider i1, i2 being Element of I such that
A2: j = i1 "/\" i2 and
A3: i1 in <.DI.) and
A4: i2 in <.i.) by A1;
i [= i2 by A4, Th15;
then i1 "/\" i [= i1 "/\" i2 by LATTICES:9;
then i1 [= i => j by A2, Def7;
hence i => j in <.DI.) by A3, Th9; :: thesis: verum