per cases ( not L is empty or L is empty ) ;
suppose A1: not L is empty ; :: thesis: id L is isomorphic
A2: id L = (id L) " by FUNCT_1:45;
id L is monotone ;
hence id L is isomorphic by A1, A2, WAYBEL_0:def 38; :: thesis: verum
end;
suppose L is empty ; :: thesis: id L is isomorphic
hence id L is isomorphic by WAYBEL_0:def 38; :: thesis: verum
end;
end;