let L be non empty lower-bounded flat LATTICE; :: thesis: for x being Element of L
for A being Chain of Bottom L,x holds card A <= 2
let x be Element of L; :: thesis: for A being Chain of Bottom L,x holds card A <= 2
let A be Chain of Bottom L,x; :: thesis: card A <= 2
S0: Bottom L <= x by YELLOW_0:44;
per cases ( Bottom L <> x or Bottom L = x ) ;
suppose KK: Bottom L <> x ; :: thesis: card A <= 2
consider b being Element of L such that
H1: ( A = {b} or A = {(Bottom L),b} ) by Thflat01;
H2: ( x in A & Bottom L in A ) by LATTICE7:def 2, S0;
A <> {b}
proof
assume A = {b} ; :: thesis: contradiction
then ( x = b & b = Bottom L ) by TARSKI:def 1, H2;
hence contradiction by KK; :: thesis: verum
end;
hence card A <= 2 by CARD_2:50, H1; :: thesis: verum
end;
suppose Bottom L = x ; :: thesis: card A <= 2
then card A = 1 by CardA1;
hence card A <= 2 ; :: thesis: verum
end;
end;