defpred S₁[ Ordinal] means $1 in { (card B1) where B1 is with_bottom CLbasis of L1 : verum } ;
A1: ex A being Ordinal st S₁[A]

proof

take card ([#] L1) ; :: thesis: S₁[ card ([#] L1)]
[#] L1 is CLbasis of L1 by YELLOW15:26;
hence S₁[ card ([#] L1)] ; :: thesis: verum

end;

consider A being Ordinal such that
A2: S₁[A] and
A3: for C being Ordinal st S₁[C] holds
A c= C from ORDINAL1:sch 1(A1);
consider B1 being with_bottom CLbasis of L1 such that
A4: A = card B1 by A2;
reconsider A = A as Cardinal by A4;
set X = { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ;
[#] L1 is CLbasis of L1 by YELLOW15:26;
then A5: card ([#] L1) in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ;

now

let x be set ; :: thesis: ( ( ( for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y ) implies x in A ) & ( x in A implies for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y ) )
thus ( ( for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y ) implies x in A ) by A2; :: thesis: ( x in A implies for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y )
assume A6: x in A ; :: thesis: for y being set st y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } holds
x in y
let y be set ; :: thesis: ( y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } implies x in y )
assume A7: y in { (card B2) where B2 is with_bottom CLbasis of L1 : verum } ; :: thesis: x in y
then consider B2 being with_bottom CLbasis of L1 such that
A8: y = card B2 ;
reconsider y1 = y as Cardinal by A8;
A c= y1 by A3, A7;
hence x in y by A6; :: thesis: verum

end;

hence meet { (card B1) where B1 is with_bottom CLbasis of L1 : verum } is Cardinal by A5, SETFAM_1:def 1; :: thesis: verum